diff options
author | Samuel Mimram <smimram@debian.org> | 2008-07-25 15:12:53 +0200 |
---|---|---|
committer | Samuel Mimram <smimram@debian.org> | 2008-07-25 15:12:53 +0200 |
commit | a0cfa4f118023d35b767a999d5a2ac4b082857b4 (patch) | |
tree | dabcac548e299fee1da464c93b3dba98484f45b1 /parsing/q_constr.ml4 | |
parent | 2281410e38ef99d025ea77194585a9bc019fdaa9 (diff) |
Imported Upstream version 8.2~beta3+dfsgupstream/8.2.beta3+dfsg
Diffstat (limited to 'parsing/q_constr.ml4')
-rw-r--r-- | parsing/q_constr.ml4 | 10 |
1 files changed, 6 insertions, 4 deletions
diff --git a/parsing/q_constr.ml4 b/parsing/q_constr.ml4 index 21c851df..72d81051 100644 --- a/parsing/q_constr.ml4 +++ b/parsing/q_constr.ml4 @@ -6,7 +6,9 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id: g_constr.ml4,v 1.58 2005/12/30 10:55:32 herbelin Exp $ *) +(*i camlp4use: "pa_extend.cmo q_MLast.cmo" i*) + +(* $Id: q_constr.ml4 10739 2008-04-01 14:45:20Z herbelin $ *) open Rawterm open Term @@ -47,9 +49,9 @@ EXTEND constr: [ "200" RIGHTA [ LIDENT "forall"; id = ident; ":"; c1 = constr; ","; c2 = constr -> - <:expr< Rawterm.RProd ($dloc$,Name $id$,$c1$,$c2$) >> + <:expr< Rawterm.RProd ($dloc$,Name $id$,Rawterm.Explicit,$c1$,$c2$) >> | "fun"; id = ident; ":"; c1 = constr; "=>"; c2 = constr -> - <:expr< Rawterm.RLambda ($dloc$,Name $id$,$c1$,$c2$) >> + <:expr< Rawterm.RLambda ($dloc$,Name $id$,Rawterm.Explicit,$c1$,$c2$) >> | "let"; id = ident; ":="; c1 = constr; "in"; c2 = constr -> <:expr< Rawterm.RLetin ($dloc$,Name $id$,$c1$,$c2$) >> (* fix todo *) @@ -59,7 +61,7 @@ EXTEND <:expr< Rawterm.RCast($dloc$,$c1$,DEFAULTcast,$c2$) >> ] | "90" RIGHTA [ c1 = constr; "->"; c2 = SELF -> - <:expr< Rawterm.RProd ($dloc$,Anonymous,$c1$,$c2$) >> ] + <:expr< Rawterm.RProd ($dloc$,Anonymous,Rawterm.Explicit,$c1$,$c2$) >> ] | "75" RIGHTA [ "~"; c = constr -> apply_ref <:expr< coq_not_ref >> [c] ] |