diff options
Diffstat (limited to 'parsing/q_constr.ml4')
| -rw-r--r-- | parsing/q_constr.ml4 | 52 |
1 files changed, 26 insertions, 26 deletions
diff --git a/parsing/q_constr.ml4 b/parsing/q_constr.ml4 index 3d203dbe..dfe7d9c0 100644 --- a/parsing/q_constr.ml4 +++ b/parsing/q_constr.ml4 @@ -1,41 +1,41 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2012 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i camlp4use: "pa_extend.cmo q_MLast.cmo" i*) +(*i camlp4deps: "tools/compat5b.cmo" i*) -(* $Id: q_constr.ml4 14641 2011-11-06 11:59:10Z herbelin $ *) - -open Rawterm +open Glob_term open Term open Names open Pattern open Q_util open Util +open Compat open Pcaml +open PcamlSig let loc = dummy_loc let dloc = <:expr< Util.dummy_loc >> let apply_ref f l = <:expr< - Rawterm.RApp ($dloc$, Rawterm.RRef ($dloc$, Lazy.force $f$), $mlexpr_of_list (fun x -> x) l$) + Glob_term.GApp ($dloc$, Glob_term.GRef ($dloc$, Lazy.force $f$), $mlexpr_of_list (fun x -> x) l$) >> EXTEND GLOBAL: expr; expr: [ [ "PATTERN"; "["; c = constr; "]" -> - <:expr< snd (Pattern.pattern_of_rawconstr $c$) >> ] ] + <:expr< snd (Pattern.pattern_of_glob_constr $c$) >> ] ] ; sort: - [ [ "Set" -> RProp Pos - | "Prop" -> RProp Null - | "Type" -> RType None ] ] + [ [ "Set" -> GProp Pos + | "Prop" -> GProp Null + | "Type" -> GType None ] ] ; ident: [ [ s = string -> <:expr< Names.id_of_string $str:s$ >> ] ] @@ -44,24 +44,24 @@ EXTEND [ [ "_" -> <:expr< Anonymous >> | id = ident -> <:expr< Name $id$ >> ] ] ; string: - [ [ UIDENT | LIDENT ] ] + [ [ s = UIDENT -> s | s = LIDENT -> s ] ] ; constr: [ "200" RIGHTA [ LIDENT "forall"; id = ident; ":"; c1 = constr; ","; c2 = constr -> - <:expr< Rawterm.RProd ($dloc$,Name $id$,Rawterm.Explicit,$c1$,$c2$) >> + <:expr< Glob_term.GProd ($dloc$,Name $id$,Glob_term.Explicit,$c1$,$c2$) >> | "fun"; id = ident; ":"; c1 = constr; "=>"; c2 = constr -> - <:expr< Rawterm.RLambda ($dloc$,Name $id$,Rawterm.Explicit,$c1$,$c2$) >> + <:expr< Glob_term.GLambda ($dloc$,Name $id$,Glob_term.Explicit,$c1$,$c2$) >> | "let"; id = ident; ":="; c1 = constr; "in"; c2 = constr -> - <:expr< Rawterm.RLetin ($dloc$,Name $id$,$c1$,$c2$) >> + <:expr< Glob_term.RLetin ($dloc$,Name $id$,$c1$,$c2$) >> (* fix todo *) ] | "100" RIGHTA [ c1 = constr; ":"; c2 = SELF -> - <:expr< Rawterm.RCast($dloc$,$c1$,DEFAULTcast,$c2$) >> ] + <:expr< Glob_term.GCast($dloc$,$c1$,DEFAULTcast,$c2$) >> ] | "90" RIGHTA [ c1 = constr; "->"; c2 = SELF -> - <:expr< Rawterm.RProd ($dloc$,Anonymous,Rawterm.Explicit,$c1$,$c2$) >> ] + <:expr< Glob_term.GProd ($dloc$,Anonymous,Glob_term.Explicit,$c1$,$c2$) >> ] | "75" RIGHTA [ "~"; c = constr -> apply_ref <:expr< coq_not_ref >> [c] ] @@ -71,15 +71,15 @@ EXTEND | "10" LEFTA [ f = constr; args = LIST1 NEXT -> let args = mlexpr_of_list (fun x -> x) args in - <:expr< Rawterm.RApp ($dloc$,$f$,$args$) >> ] + <:expr< Glob_term.GApp ($dloc$,$f$,$args$) >> ] | "0" - [ s = sort -> <:expr< Rawterm.RSort ($dloc$,s) >> - | id = ident -> <:expr< Rawterm.RVar ($dloc$,$id$) >> - | "_" -> <:expr< Rawterm.RHole ($dloc$, QuestionMark (Define False)) >> - | "?"; id = ident -> <:expr< Rawterm.RPatVar($dloc$,(False,$id$)) >> + [ s = sort -> <:expr< Glob_term.GSort ($dloc$,s) >> + | id = ident -> <:expr< Glob_term.GVar ($dloc$,$id$) >> + | "_" -> <:expr< Glob_term.GHole ($dloc$, QuestionMark (Define False)) >> + | "?"; id = ident -> <:expr< Glob_term.GPatVar($dloc$,(False,$id$)) >> | "{"; c1 = constr; "}"; "+"; "{"; c2 = constr; "}" -> apply_ref <:expr< coq_sumbool_ref >> [c1;c2] - | "%"; e = string -> <:expr< Rawterm.RRef ($dloc$,Lazy.force $lid:e$) >> + | "%"; e = string -> <:expr< Glob_term.GRef ($dloc$,Lazy.force $lid:e$) >> | c = match_constr -> c | "("; c = constr LEVEL "200"; ")" -> c ] ] ; @@ -87,7 +87,7 @@ EXTEND [ [ "match"; c = constr LEVEL "100"; (ty,nal) = match_type; "with"; OPT"|"; br = LIST0 eqn SEP "|"; "end" -> let br = mlexpr_of_list (fun x -> x) br in - <:expr< Rawterm.RCases ($dloc$,$ty$,[($c$,$nal$)],$br$) >> + <:expr< Glob_term.GCases ($dloc$,$ty$,[($c$,$nal$)],$br$) >> ] ] ; match_type: @@ -108,13 +108,13 @@ EXTEND [ [ "%"; e = string; lip = LIST0 patvar -> let lp = mlexpr_of_list (fun (_,x) -> x) lip in let lid = List.flatten (List.map fst lip) in - lid, <:expr< Rawterm.PatCstr ($dloc$,$lid:e$,$lp$,Anonymous) >> + lid, <:expr< Glob_term.PatCstr ($dloc$,$lid:e$,$lp$,Anonymous) >> | p = patvar -> p | "("; p = pattern; ")" -> p ] ] ; patvar: - [ [ "_" -> [], <:expr< Rawterm.PatVar ($dloc$,Anonymous) >> - | id = ident -> [id], <:expr< Rawterm.PatVar ($dloc$,Name $id$) >> + [ [ "_" -> [], <:expr< Glob_term.PatVar ($dloc$,Anonymous) >> + | id = ident -> [id], <:expr< Glob_term.PatVar ($dloc$,Name $id$) >> ] ] ; END;; |