Commit 0207232e authored by charguer's avatar charguer
Browse files

todolist

parent 900ad9a8
-- xfor_inv prefers to use b-1 as upper bound if possible
-- xapp as b'
-- xapp on a leaf does not do xpull
- xfor_inv tag goal
-- case_if checking single goal
-- xmatch_no_intros should do the inversion.
-- improve xauto spec
-- xcf_show without argument should put at head of goal
-- xunfold at fait pas le unfold
-- Ouvrir liblistZ à la fin de cflib
-- Demo de la notation pour les records
-- Array : compléter.
-- LibListZ.sub
-- Array.iter forall l, Array xs \c I l
-- renommer Array.of_list
-- utiliser "of_list []" à la place de make_empty
-- régler le "==>"
-- avoir un flag pour _output
-- external sur une constante, passe pas le typeur
-- ajouter
- documenter la faiblesse de Array.make
- remettre les vrais noms des external
- xclose with args for the change.
......
......@@ -4,6 +4,19 @@ Require Import Demo_ml.
Require Import Stdlib.
Open Scope tag_scope.
(*
Notation "P1 '==>' P2" :=
(@pred_le heap P1 P2) (at level 55,
format "'[' '[' P1 ']' '/' '==>' '/' '[' P2 ']' ']'" )
: charac.
Notation "Q1 '===>' Q2" :=
(@rel_le _ heap Q1 Q2) (at level 69,
format "'[' '[' Q1 ']' '/' '===>' '/' '[' Q2 ']' ']'")
: charac.
*)
(********************************************************************)
......
......@@ -1129,11 +1129,11 @@ Tactic Notation "xunfold" constr(E) "at" constr(n) :=
| |- context [ hdata' (E' _ _ _ _ _) _ ] => constr:(true)
| |- context [ hdata' (E' _ _ _ _ _ _) _ ] => constr:(true)
| |- context [ hdata' (E' _ _ _ _ _ _ _) _ ] => constr:(true)
| |- context [ hdata' (E _ _ _ _ _ _ _ _) _ ] => constr:(true)
| |- context [ hdata' (E _ _ _ _ _ _ _ _ _) _ ] => constr:(true)
| |- context [ hdata' (E _ _ _ _ _ _ _ _ _ _) _ ] => constr:(true)
| |- context [ hdata' (E _ _ _ _ _ _ _ _ _ _ _) _ ] => constr:(true)
| |- context [ hdata' (E _ _ _ _ _ _ _ _ _ _ _ _) _ ] => constr:(true)
| |- context [ hdata' (E' _ _ _ _ _ _ _ _) _ ] => constr:(true)
| |- context [ hdata' (E' _ _ _ _ _ _ _ _ _) _ ] => constr:(true)
| |- context [ hdata' (E' _ _ _ _ _ _ _ _ _ _) _ ] => constr:(true)
| |- context [ hdata' (E' _ _ _ _ _ _ _ _ _ _ _) _ ] => constr:(true)
| |- context [ hdata' (E' _ _ _ _ _ _ _ _ _ _ _ _) _ ] => constr:(true)
| _ => constr:(false)
end in
match ok with
......
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment