diff options
| author |  letouzey <letouzey@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2012-05-29 11:08:37 +0000 |
|---|---|---|
| committer | letouzey <letouzey@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2012-05-29 11:08:37 +0000 |
| commit | 5fa47f1258408541150e2e4c26d60ff694e7c1bc (patch) | |
| tree | 9e7aee1ea714cebdccc50dbd85735948d8baeaf0 /parsing/q_constr.ml4 | |
| parent | 45038a0bfd5621153ba0dd4b6e06755fd15da1e3 (diff) | |
locus.mli for occurrences+clauses, misctypes.mli for various little things
Corresponding operations in locusops.ml and miscops.ml
The type of occurrences is now a clear algebraic one instead of
a bool*list hard to understand.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15372 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'parsing/q_constr.ml4')
| -rw-r--r-- | parsing/q_constr.ml4 | 11 |
1 files changed, 6 insertions, 5 deletions
diff --git a/parsing/q_constr.ml4 b/parsing/q_constr.ml4 index f5225feb3..543240a82 100644 --- a/parsing/q_constr.ml4 +++ b/parsing/q_constr.ml4 @@ -17,6 +17,7 @@ open Pp open Compat open Pcaml open PcamlSig +open Misctypes let loc = dummy_loc let dloc = <:expr< Pp.dummy_loc >> @@ -33,8 +34,8 @@ EXTEND <:expr< snd (Pattern.pattern_of_glob_constr $c$) >> ] ] ; sort: - [ [ "Set" -> GProp Pos - | "Prop" -> GProp Null + [ [ "Set" -> GSet + | "Prop" -> GProp | "Type" -> GType None ] ] ; ident: @@ -49,9 +50,9 @@ EXTEND constr: [ "200" RIGHTA [ LIDENT "forall"; id = ident; ":"; c1 = constr; ","; c2 = constr -> - <:expr< Glob_term.GProd ($dloc$,Name $id$,Glob_term.Explicit,$c1$,$c2$) >> + <:expr< Glob_term.GProd ($dloc$,Name $id$,Decl_kinds.Explicit,$c1$,$c2$) >> | "fun"; id = ident; ":"; c1 = constr; "=>"; c2 = constr -> - <:expr< Glob_term.GLambda ($dloc$,Name $id$,Glob_term.Explicit,$c1$,$c2$) >> + <:expr< Glob_term.GLambda ($dloc$,Name $id$,Decl_kinds.Explicit,$c1$,$c2$) >> | "let"; id = ident; ":="; c1 = constr; "in"; c2 = constr -> <:expr< Glob_term.RLetin ($dloc$,Name $id$,$c1$,$c2$) >> (* fix todo *) @@ -61,7 +62,7 @@ EXTEND <:expr< Glob_term.GCast($dloc$,$c1$,DEFAULTcast,$c2$) >> ] | "90" RIGHTA [ c1 = constr; "->"; c2 = SELF -> - <:expr< Glob_term.GProd ($dloc$,Anonymous,Glob_term.Explicit,$c1$,$c2$) >> ] + <:expr< Glob_term.GProd ($dloc$,Anonymous,Decl_kinds.Explicit,$c1$,$c2$) >> ] | "75" RIGHTA [ "~"; c = constr -> apply_ref <:expr< coq_not_ref >> [c] ] |