diff options
| author |  glondu <glondu@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2010-12-23 18:51:08 +0000 |
|---|---|---|
| committer | glondu <glondu@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2010-12-23 18:51:08 +0000 |
| commit | 6f60984128d38d1166000223f369fdeb1c6af1a3 (patch) | |
| tree | c2a5d166349ef6d643ce8a76b7fd3f84ee9f6cb9 | |
| parent | 8f9461509338a3ebba46faaad3116c4e44135423 (diff) | |
Rename rawterm.ml into glob_term.ml
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13744 85f007b7-540e-0410-9357-904b9bb8a0f7
152 files changed, 321 insertions, 321 deletions
diff --git a/dev/base_include b/dev/base_include index 19c0f4b4e..18c5c324a 100644 --- a/dev/base_include +++ b/dev/base_include @@ -79,7 +79,7 @@ open Cbv open Classops open Clenv open Clenvtac -open Rawterm +open Glob_term open Coercion open Coercion.Default open Recordops diff --git a/dev/printers.mllib b/dev/printers.mllib index a244b7979..9403a4cca 100644 --- a/dev/printers.mllib +++ b/dev/printers.mllib @@ -67,7 +67,7 @@ Heads Termops Namegen Evd -Rawterm +Glob_term Reductionops Inductiveops Retyping diff --git a/interp/constrextern.ml b/interp/constrextern.ml index 4029f6150..9215f9b51 100644 --- a/interp/constrextern.ml +++ b/interp/constrextern.ml @@ -21,7 +21,7 @@ open Environ open Libnames open Impargs open Topconstr -open Rawterm +open Glob_term open Pattern open Nametab open Notation @@ -743,7 +743,7 @@ and extern_eqn inctx scopes vars (loc,ids,pl,c) = and extern_symbol (tmp_scope,scopes as allscopes) vars t = function | [] -> raise No_match | (keyrule,pat,n as _rule)::rules -> - let loc = Rawterm.loc_of_glob_constr t in + let loc = Glob_term.loc_of_glob_constr t in try (* Adjusts to the number of arguments expected by the notation *) let (t,args,argsscopes,argsimpls) = match t,n with diff --git a/interp/constrextern.mli b/interp/constrextern.mli index 979c974ac..033090fc9 100644 --- a/interp/constrextern.mli +++ b/interp/constrextern.mli @@ -14,7 +14,7 @@ open Sign open Environ open Libnames open Nametab -open Rawterm +open Glob_term open Pattern open Topconstr open Notation diff --git a/interp/constrintern.ml b/interp/constrintern.ml index c097ce43d..4e8d0a621 100644 --- a/interp/constrintern.ml +++ b/interp/constrintern.ml @@ -14,7 +14,7 @@ open Nameops open Namegen open Libnames open Impargs -open Rawterm +open Glob_term open Pattern open Pretyping open Cases diff --git a/interp/constrintern.mli b/interp/constrintern.mli index cf9e899a6..59afcd313 100644 --- a/interp/constrintern.mli +++ b/interp/constrintern.mli @@ -12,7 +12,7 @@ open Sign open Evd open Environ open Libnames -open Rawterm +open Glob_term open Pattern open Topconstr open Termops @@ -82,7 +82,7 @@ val intern_gen : bool -> evar_map -> env -> val intern_pattern : env -> cases_pattern_expr -> Names.identifier list * - ((Names.identifier * Names.identifier) list * Rawterm.cases_pattern) list + ((Names.identifier * Names.identifier) list * Glob_term.cases_pattern) list val intern_context : bool -> evar_map -> env -> local_binder list -> glob_binder list diff --git a/interp/genarg.ml b/interp/genarg.ml index 23e17a2d4..e564bd11e 100644 --- a/interp/genarg.ml +++ b/interp/genarg.ml @@ -11,7 +11,7 @@ open Util open Names open Nameops open Nametab -open Rawterm +open Glob_term open Topconstr open Term open Evd diff --git a/interp/genarg.mli b/interp/genarg.mli index 231126d44..3c825212f 100644 --- a/interp/genarg.mli +++ b/interp/genarg.mli @@ -10,7 +10,7 @@ open Util open Names open Term open Libnames -open Rawterm +open Glob_term open Pattern open Topconstr open Term diff --git a/interp/implicit_quantifiers.ml b/interp/implicit_quantifiers.ml index 864e521bf..b430c000b 100644 --- a/interp/implicit_quantifiers.ml +++ b/interp/implicit_quantifiers.ml @@ -16,7 +16,7 @@ open Environ open Nametab open Mod_subst open Util -open Rawterm +open Glob_term open Topconstr open Libnames open Typeclasses diff --git a/interp/implicit_quantifiers.mli b/interp/implicit_quantifiers.mli index 4c73edbf7..cb782e0c5 100644 --- a/interp/implicit_quantifiers.mli +++ b/interp/implicit_quantifiers.mli @@ -14,7 +14,7 @@ open Evd open Environ open Nametab open Mod_subst -open Rawterm +open Glob_term open Topconstr open Util open Libnames @@ -42,7 +42,7 @@ val generalizable_vars_of_glob_constr : ?bound:Idset.t -> ?allowed:Idset.t -> val make_fresh : Names.Idset.t -> Environ.env -> identifier -> identifier -val implicits_of_rawterm : ?with_products:bool -> Rawterm.glob_constr -> (Topconstr.explicitation * (bool * bool * bool)) list +val implicits_of_rawterm : ?with_products:bool -> Glob_term.glob_constr -> (Topconstr.explicitation * (bool * bool * bool)) list val combine_params_freevar : Names.Idset.t -> (global_reference * bool) option * (Names.name * Term.constr option * Term.types) -> diff --git a/interp/notation.ml b/interp/notation.ml index eea8afeef..37c9ddbeb 100644 --- a/interp/notation.ml +++ b/interp/notation.ml @@ -15,7 +15,7 @@ open Term open Nametab open Libnames open Summary -open Rawterm +open Glob_term open Topconstr open Ppextend (*i*) diff --git a/interp/notation.mli b/interp/notation.mli index 290d5f3df..52a7c2b99 100644 --- a/interp/notation.mli +++ b/interp/notation.mli @@ -12,7 +12,7 @@ open Bigint open Names open Nametab open Libnames -open Rawterm +open Glob_term open Topconstr open Ppextend diff --git a/interp/reserve.ml b/interp/reserve.ml index 9d20236b8..c143b5710 100644 --- a/interp/reserve.ml +++ b/interp/reserve.ml @@ -46,7 +46,7 @@ let declare_reserved_type (loc,id) t = let find_reserved_type id = Idmap.find (root_of_id id) !reserve_table -open Rawterm +open Glob_term let rec unloc = function | GVar (_,id) -> GVar (dummy_loc,id) diff --git a/interp/reserve.mli b/interp/reserve.mli index 1766f77b9..0e43e5283 100644 --- a/interp/reserve.mli +++ b/interp/reserve.mli @@ -8,7 +8,7 @@ open Util open Names -open Rawterm +open Glob_term open Topconstr val declare_reserved_type : identifier located -> aconstr -> unit diff --git a/interp/syntax_def.mli b/interp/syntax_def.mli index 21ea7390b..e4da52a33 100644 --- a/interp/syntax_def.mli +++ b/interp/syntax_def.mli @@ -9,7 +9,7 @@ open Util open Names open Topconstr -open Rawterm +open Glob_term open Nametab open Libnames diff --git a/interp/topconstr.ml b/interp/topconstr.ml index 61549cb1f..0e0326808 100644 --- a/interp/topconstr.ml +++ b/interp/topconstr.ml @@ -12,7 +12,7 @@ open Util open Names open Nameops open Libnames -open Rawterm +open Glob_term open Term open Mod_subst (*i*) diff --git a/interp/topconstr.mli b/interp/topconstr.mli index 6e8769b85..b01c35093 100644 --- a/interp/topconstr.mli +++ b/interp/topconstr.mli @@ -10,7 +10,7 @@ open Pp open Util open Names open Libnames -open Rawterm +open Glob_term open Term open Mod_subst diff --git a/parsing/egrammar.mli b/parsing/egrammar.mli index 1adc06cbe..1d85c74e5 100644 --- a/parsing/egrammar.mli +++ b/parsing/egrammar.mli @@ -14,7 +14,7 @@ open Pcoq open Extend open Vernacexpr open Ppextend -open Rawterm +open Glob_term open Genarg open Mod_subst diff --git a/parsing/g_constr.ml4 b/parsing/g_constr.ml4 index 12cffc492..d8574409d 100644 --- a/parsing/g_constr.ml4 +++ b/parsing/g_constr.ml4 @@ -10,7 +10,7 @@ open Pp open Pcoq open Constr open Prim -open Rawterm +open Glob_term open Term open Names open Libnames @@ -33,7 +33,7 @@ let mk_cast = function let binders_of_lidents l = List.map (fun (loc, id) -> - LocalRawAssum ([loc, Name id], Default Rawterm.Explicit, + LocalRawAssum ([loc, Name id], Default Glob_term.Explicit, CHole (loc, Some (Evd.BinderType (Name id))))) l let mk_fixb (id,bl,ann,body,(loc,tyc)) = diff --git a/parsing/g_ltac.ml4 b/parsing/g_ltac.ml4 index d2f05d4ef..1d100c7cc 100644 --- a/parsing/g_ltac.ml4 +++ b/parsing/g_ltac.ml4 @@ -9,7 +9,7 @@ open Pp open Util open Topconstr -open Rawterm +open Glob_term open Tacexpr open Vernacexpr open Pcoq diff --git a/parsing/g_proofs.ml4 b/parsing/g_proofs.ml4 index e23ef9143..2b6759aed 100644 --- a/parsing/g_proofs.ml4 +++ b/parsing/g_proofs.ml4 @@ -126,6 +126,6 @@ GEXTEND Gram ; constr_body: [ [ ":="; c = lconstr -> c - | ":"; t = lconstr; ":="; c = lconstr -> CCast(loc,c, Rawterm.CastConv (Term.DEFAULTcast,t)) ] ] + | ":"; t = lconstr; ":="; c = lconstr -> CCast(loc,c, Glob_term.CastConv (Term.DEFAULTcast,t)) ] ] ; END diff --git a/parsing/g_tactic.ml4 b/parsing/g_tactic.ml4 index 9b476d996..9f4b10575 100644 --- a/parsing/g_tactic.ml4 +++ b/parsing/g_tactic.ml4 @@ -10,7 +10,7 @@ open Pp open Pcoq open Util open Tacexpr -open Rawterm +open Glob_term open Genarg open Topconstr open Libnames @@ -165,8 +165,8 @@ let mkCLambdaN_simple bl c = let loc_of_ne_list l = join_loc (fst (List.hd l)) (fst (list_last l)) let map_int_or_var f = function - | Rawterm.ArgArg x -> Rawterm.ArgArg (f x) - | Rawterm.ArgVar _ as y -> y + | Glob_term.ArgArg x -> Glob_term.ArgArg (f x) + | Glob_term.ArgVar _ as y -> y let all_concl_occs_clause = { onhyps=Some[]; concl_occs=all_occurrences_expr } @@ -204,12 +204,12 @@ GEXTEND Gram simple_intropattern; int_or_var: - [ [ n = integer -> Rawterm.ArgArg n - | id = identref -> Rawterm.ArgVar id ] ] + [ [ n = integer -> Glob_term.ArgArg n + | id = identref -> Glob_term.ArgVar id ] ] ; nat_or_var: - [ [ n = natural -> Rawterm.ArgArg n - | id = identref -> Rawterm.ArgVar id ] ] + [ [ n = natural -> Glob_term.ArgArg n + | id = identref -> Glob_term.ArgVar id ] ] ; (* An identifier or a quotation meta-variable *) id_or_meta: diff --git a/parsing/g_vernac.ml4 b/parsing/g_vernac.ml4 index f23b835e1..e42fc7599 100644 --- a/parsing/g_vernac.ml4 +++ b/parsing/g_vernac.ml4 @@ -241,7 +241,7 @@ GEXTEND Gram def_body: [ [ bl = binders; ":="; red = reduce; c = lconstr -> (match c with - CCast(_,c, Rawterm.CastConv (Term.DEFAULTcast,t)) -> DefineBody (bl, red, c, Some t) + CCast(_,c, Glob_term.CastConv (Term.DEFAULTcast,t)) -> DefineBody (bl, red, c, Some t) | _ -> DefineBody (bl, red, c, None)) | bl = binders; ":"; t = lconstr; ":="; red = reduce; c = lconstr -> DefineBody (bl, red, c, Some t) @@ -343,7 +343,7 @@ GEXTEND Gram (oc,DefExpr (id,mkCLambdaN loc l b,Some (mkCProdN loc l t))) | l = binders; ":="; b = lconstr -> fun id -> match b with - | CCast(_,b, Rawterm.CastConv (_, t)) -> + | CCast(_,b, Glob_term.CastConv (_, t)) -> (false,DefExpr(id,mkCLambdaN loc l b,Some (mkCProdN loc l t))) | _ -> (false,DefExpr(id,mkCLambdaN loc l b,None)) ] ] @@ -543,7 +543,7 @@ GEXTEND Gram VernacContext c | IDENT "Instance"; namesup = instance_name; ":"; - expl = [ "!" -> Rawterm.Implicit | -> Rawterm.Explicit ] ; t = operconstr LEVEL "200"; + expl = [ "!" -> Glob_term.Implicit | -> Glob_term.Explicit ] ; t = operconstr LEVEL "200"; pri = OPT [ "|"; i = natural -> i ] ; props = [ ":="; "{"; r = record_declaration; "}" -> r | ":="; c = lconstr -> c | -> CRecord (loc, None, []) ] -> @@ -614,7 +614,7 @@ GEXTEND Gram (* Hack! Should be in grammar_ext, but camlp4 factorize badly *) | IDENT "Declare"; IDENT "Instance"; namesup = instance_name; ":"; - expl = [ "!" -> Rawterm.Implicit | -> Rawterm.Explicit ] ; t = operconstr LEVEL "200"; + expl = [ "!" -> Glob_term.Implicit | -> Glob_term.Explicit ] ; t = operconstr LEVEL "200"; pri = OPT [ "|"; i = natural -> i ] -> VernacInstance (true, not (use_non_locality ()), snd namesup, (fst namesup, expl, t), @@ -721,7 +721,7 @@ GEXTEND Gram [ [ IDENT "Eval"; r = Tactic.red_expr; "in"; c = lconstr -> fun g -> VernacCheckMayEval (Some r, g, c) | IDENT "Compute"; c = lconstr -> - fun g -> VernacCheckMayEval (Some Rawterm.CbvVm, g, c) + fun g -> VernacCheckMayEval (Some Glob_term.CbvVm, g, c) | IDENT "Check"; c = lconstr -> fun g -> VernacCheckMayEval (None, g, c) ] ] ; diff --git a/parsing/g_xml.ml4 b/parsing/g_xml.ml4 index de3fbb683..18bc1ff78 100644 --- a/parsing/g_xml.ml4 +++ b/parsing/g_xml.ml4 @@ -11,7 +11,7 @@ open Util open Names open Term open Pcoq -open Rawterm +open Glob_term open Genarg open Tacexpr open Libnames diff --git a/parsing/grammar.mllib b/parsing/grammar.mllib index 98905d3c0..02e27827b 100644 --- a/parsing/grammar.mllib +++ b/parsing/grammar.mllib @@ -59,7 +59,7 @@ Namegen Evd Reductionops Inductiveops -Rawterm +Glob_term Detyping Pattern Topconstr diff --git a/parsing/pcoq.ml4 b/parsing/pcoq.ml4 index 50cbd3145..eb1a69610 100644 --- a/parsing/pcoq.ml4 +++ b/parsing/pcoq.ml4 @@ -13,7 +13,7 @@ open Util open Names open Extend open Libnames -open Rawterm +open Glob_term open Topconstr open Genarg open Tacexpr diff --git a/parsing/pcoq.mli b/parsing/pcoq.mli index 7db89a5ff..68d434a2b 100644 --- a/parsing/pcoq.mli +++ b/parsing/pcoq.mli @@ -8,7 +8,7 @@ open Util open Names -open Rawterm +open Glob_term open Extend open Vernacexpr open Genarg @@ -209,7 +209,7 @@ module Module : module Tactic : sig - open Rawterm + open Glob_term val open_constr : open_constr_expr Gram.entry val casted_open_constr : open_constr_expr Gram.entry val constr_with_bindings : constr_expr with_bindings Gram.entry diff --git a/parsing/ppconstr.ml b/parsing/ppconstr.ml index 9bfa32285..9e9d21a3d 100644 --- a/parsing/ppconstr.ml +++ b/parsing/ppconstr.ml @@ -17,7 +17,7 @@ open Ppextend open Topconstr open Term open Pattern -open Rawterm +open Glob_term open Constrextern open Termops (*i*) diff --git a/parsing/ppconstr.mli b/parsing/ppconstr.mli index 304738599..49791d595 100644 --- a/parsing/ppconstr.mli +++ b/parsing/ppconstr.mli @@ -11,7 +11,7 @@ open Environ open Term open Libnames open Pcoq -open Rawterm +open Glob_term open Topconstr open Names open Util diff --git a/parsing/pptactic.ml b/parsing/pptactic.ml index 0dea0d2ac..015dc9c08 100644 --- a/parsing/pptactic.ml +++ b/parsing/pptactic.ml @@ -11,7 +11,7 @@ open Names open Namegen open Util open Tacexpr -open Rawterm +open Glob_term open Topconstr open Genarg open Libnames @@ -958,7 +958,7 @@ let strip_prod_binders_rawterm n (ty,_) = let rec strip_ty acc n ty = if n=0 then (List.rev acc, (ty,None)) else match ty with - Rawterm.GProd(loc,na,Explicit,a,b) -> + Glob_term.GProd(loc,na,Explicit,a,b) -> strip_ty (([dummy_loc,na],(a,None))::acc) (n-1) b | _ -> error "Cannot translate fix tactic: not enough products" in strip_ty [] n ty diff --git a/parsing/pptactic.mli b/parsing/pptactic.mli index 21de95ba0..d85f1ec3f 100644 --- a/parsing/pptactic.mli +++ b/parsing/pptactic.mli @@ -12,7 +12,7 @@ open Tacexpr open Pretyping open Proof_type open Topconstr -open Rawterm +open Glob_term open Pattern open Ppextend open Environ diff --git a/parsing/ppvernac.ml b/parsing/ppvernac.ml index 0a65578f1..3d3e10456 100644 --- a/parsing/ppvernac.ml +++ b/parsing/ppvernac.ml @@ -16,7 +16,7 @@ open Extend open Vernacexpr open Ppconstr open Pptactic -open Rawterm +open Glob_term open Genarg open Pcoq open Libnames diff --git a/parsing/ppvernac.mli b/parsing/ppvernac.mli index d0d8a572d..7801de6a2 100644 --- a/parsing/ppvernac.mli +++ b/parsing/ppvernac.mli @@ -15,7 +15,7 @@ open Nametab open Util open Ppconstr open Pptactic -open Rawterm +open Glob_term open Pcoq open Libnames open Ppextend diff --git a/parsing/printer.mli b/parsing/printer.mli index 2da367816..ca91cfd4f 100644 --- a/parsing/printer.mli +++ b/parsing/printer.mli @@ -12,13 +12,13 @@ open Libnames open Term open Sign open Environ -open Rawterm +open Glob_term open Pattern open Nametab open Termops open Evd open Proof_type -open Rawterm +open Glob_term open Tacexpr (** These are the entry points for printing terms, context, tac, ... *) diff --git a/parsing/q_constr.ml4 b/parsing/q_constr.ml4 index 7b0576a32..c8451afb1 100644 --- a/parsing/q_constr.ml4 +++ b/parsing/q_constr.ml4 @@ -8,7 +8,7 @@ (*i camlp4deps: "tools/compat5b.cmo" i*) -open Rawterm +open Glob_term open Term open Names open Pattern @@ -23,7 +23,7 @@ let dloc = <:expr< Util.dummy_loc >> let apply_ref f l = <:expr< - Rawterm.GApp ($dloc$, Rawterm.GRef ($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 @@ -49,19 +49,19 @@ EXTEND constr: [ "200" RIGHTA [ LIDENT "forall"; id = ident; ":"; c1 = constr; ","; c2 = constr -> - <:expr< Rawterm.GProd ($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.GLambda ($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.GCast($dloc$,$c1$,DEFAULTcast,$c2$) >> ] + <:expr< Glob_term.GCast($dloc$,$c1$,DEFAULTcast,$c2$) >> ] | "90" RIGHTA [ c1 = constr; "->"; c2 = SELF -> - <:expr< Rawterm.GProd ($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.GApp ($dloc$,$f$,$args$) >> ] + <:expr< Glob_term.GApp ($dloc$,$f$,$args$) >> ] | "0" - [ s = sort -> <:expr< Rawterm.GSort ($dloc$,s) >> - | id = ident -> <:expr< Rawterm.GVar ($dloc$,$id$) >> - | "_" -> <:expr< Rawterm.GHole ($dloc$, QuestionMark (Define False)) >> - | "?"; id = ident -> <:expr< Rawterm.GPatVar($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.GRef ($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.GCases ($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;; diff --git a/parsing/q_coqast.ml4 b/parsing/q_coqast.ml4 index bf7f94587..d5ffa6457 100644 --- a/parsing/q_coqast.ml4 +++ b/parsing/q_coqast.ml4 @@ -72,12 +72,12 @@ let mlexpr_of_or_metaid f = function | Tacexpr.MetaId (_,id) -> <:expr< Tacexpr.AI $anti loc id$ >> let mlexpr_of_quantified_hypothesis = function - | Rawterm.AnonHyp n -> <:expr< Rawterm.AnonHyp $mlexpr_of_int n$ >> - | Rawterm.NamedHyp id -> <:expr< Rawterm.NamedHyp $mlexpr_of_ident id$ >> + | Glob_term.AnonHyp n -> <:expr< Glob_term.AnonHyp $mlexpr_of_int n$ >> + | Glob_term.NamedHyp id -> <:expr< Glob_term.NamedHyp $mlexpr_of_ident id$ >> let mlexpr_of_or_var f = function - | Rawterm.ArgArg x -> <:expr< Rawterm.ArgArg $f x$ >> - | Rawterm.ArgVar id -> <:expr< Rawterm.ArgVar $mlexpr_of_located mlexpr_of_ident id$ >> + | Glob_term.ArgArg x -> <:expr< Glob_term.ArgArg $f x$ >> + | Glob_term.ArgVar id -> <:expr< Glob_term.ArgVar $mlexpr_of_located mlexpr_of_ident id$ >> let mlexpr_of_hyp = mlexpr_of_or_metaid (mlexpr_of_located mlexpr_of_ident) @@ -102,17 +102,17 @@ let mlexpr_of_clause cl = Tacexpr.concl_occs= $mlexpr_of_occs cl.Tacexpr.concl_occs$} >> let mlexpr_of_red_flags { - Rawterm.rBeta = bb; - Rawterm.rIota = bi; - Rawterm.rZeta = bz; - Rawterm.rDelta = bd; - Rawterm.rConst = l + Glob_term.rBeta = bb; + Glob_term.rIota = bi; + Glob_term.rZeta = bz; + Glob_term.rDelta = bd; + Glob_term.rConst = l } = <:expr< { - Rawterm.rBeta = $mlexpr_of_bool bb$; - Rawterm.rIota = $mlexpr_of_bool bi$; - Rawterm.rZeta = $mlexpr_of_bool bz$; - Rawterm.rDelta = $mlexpr_of_bool bd$; - Rawterm.rConst = $mlexpr_of_list (mlexpr_of_by_notation mlexpr_of_reference) l$ + Glob_term.rBeta = $mlexpr_of_bool bb$; + Glob_term.rIota = $mlexpr_of_bool bi$; + Glob_term.rZeta = $mlexpr_of_bool bz$; + Glob_term.rDelta = $mlexpr_of_bool bd$; + Glob_term.rConst = $mlexpr_of_list (mlexpr_of_by_notation mlexpr_of_reference) l$ } >> let mlexpr_of_explicitation = function @@ -120,8 +120,8 @@ let mlexpr_of_explicitation = function | Topconstr.ExplByPos (n,_id) -> <:expr< Topconstr.ExplByPos $mlexpr_of_int n$ >> let mlexpr_of_binding_kind = function - | Rawterm.Implicit -> <:expr< Rawterm.Implicit >> - | Rawterm.Explicit -> <:expr< Rawterm.Explicit >> + | Glob_term.Implicit -> <:expr< Glob_term.Implicit >> + | Glob_term.Explicit -> <:expr< Glob_term.Explicit >> let mlexpr_of_binder_kind = function | Topconstr.Default b -> <:expr< Topconstr.Default $mlexpr_of_binding_kind b$ >> @@ -158,25 +158,25 @@ let mlexpr_of_occ_constr = mlexpr_of_occurrences mlexpr_of_constr let mlexpr_of_red_expr = function - | Rawterm.Red b -> <:expr< Rawterm.Red $mlexpr_of_bool b$ >> - | Rawterm.Hnf -> <:expr< Rawterm.Hnf >> - | Rawterm.Simpl o -> <:expr< Rawterm.Simpl $mlexpr_of_option mlexpr_of_occ_constr o$ >> - | Rawterm.Cbv f -> - <:expr< Rawterm.Cbv $mlexpr_of_red_flags f$ >> - | Rawterm.Lazy f -> - <:expr< Rawterm.Lazy $mlexpr_of_red_flags f$ >> - | Rawterm.Unfold l -> + | Glob_term.Red b -> <:expr< Glob_term.Red $mlexpr_of_bool b$ >> + | Glob_term.Hnf -> <:expr< Glob_term.Hnf >> + | Glob_term.Simpl o -> <:expr< Glob_term.Simpl $mlexpr_of_option mlexpr_of_occ_constr o$ >> + | Glob_term.Cbv f -> + <:expr< Glob_term.Cbv $mlexpr_of_red_flags f$ >> + | Glob_term.Lazy f -> + <:expr< Glob_term.Lazy $mlexpr_of_red_flags f$ >> + | Glob_term.Unfold l -> let f1 = mlexpr_of_by_notation mlexpr_of_reference in let f = mlexpr_of_list (mlexpr_of_occurrences f1) in - <:expr< Rawterm.Unfold $f l$ >> - | Rawterm.Fold l -> - <:expr< Rawterm.Fold $mlexpr_of_list mlexpr_of_constr l$ >> - | Rawterm.Pattern l -> + <:expr< Glob_term.Unfold $f l$ >> + | Glob_term.Fold l -> + <:expr< Glob_term.Fold $mlexpr_of_list mlexpr_of_constr l$ >> + | Glob_term.Pattern l -> let f = mlexpr_of_list mlexpr_of_occ_constr in - <:expr< Rawterm.Pattern $f l$ >> - | Rawterm.CbvVm -> <:expr< Rawterm.CbvVm >> - | Rawterm.ExtraRedExpr s -> - <:expr< Rawterm.ExtraRedExpr $mlexpr_of_string s$ >> + <:expr< Glob_term.Pattern $f l$ >> + | Glob_term.CbvVm -> <:expr< Glob_term.CbvVm >> + | Glob_term.ExtraRedExpr s -> + <:expr< Glob_term.ExtraRedExpr $mlexpr_of_string s$ >> let rec mlexpr_of_argtype loc = function | Genarg.BoolArgType -> <:expr< Genarg.BoolArgType >> @@ -206,25 +206,25 @@ let rec mlexpr_of_argtype loc = function | Genarg.ExtraArgType s -> <:expr< Genarg.ExtraArgType $str:s$ >> let rec mlexpr_of_may_eval f = function - | Rawterm.ConstrEval (r,c) -> - <:expr< Rawterm.ConstrEval $mlexpr_of_red_expr r$ $f c$ >> - | Rawterm.ConstrContext ((loc,id),c) -> + | Glob_term.ConstrEval (r,c) -> + <:expr< Glob_term.ConstrEval $mlexpr_of_red_expr r$ $f c$ >> + | Glob_term.ConstrContext ((loc,id),c) -> let id = mlexpr_of_ident id in - <:expr< Rawterm.ConstrContext (loc,$id$) $f c$ >> - | Rawterm.ConstrTypeOf c -> - <:expr< Rawterm.ConstrTypeOf $mlexpr_of_constr c$ >> - | Rawterm.ConstrTerm c -> - <:expr< Rawterm.ConstrTerm $mlexpr_of_constr c$ >> + <:expr< Glob_term.ConstrContext (loc,$id$) $f c$ >> + | Glob_term.ConstrTypeOf c -> + <:expr< Glob_term.ConstrTypeOf $mlexpr_of_constr c$ >> + | Glob_term.ConstrTerm c -> + <:expr< Glob_term.ConstrTerm $mlexpr_of_constr c$ >> let mlexpr_of_binding_kind = function - | Rawterm.ExplicitBindings l -> + | Glob_term.ExplicitBindings l -> let l = mlexpr_of_list (mlexpr_of_triple mlexpr_of_loc mlexpr_of_quantified_hypothesis mlexpr_of_constr) l in - <:expr< Rawterm.ExplicitBindings $l$ >> - | Rawterm.ImplicitBindings l -> + <:expr< Glob_term.ExplicitBindings $l$ >> + | Glob_term.ImplicitBindings l -> let l = mlexpr_of_list mlexpr_of_constr l in - <:expr< Rawterm.ImplicitBindings $l$ >> - | Rawterm.NoBindings -> - <:expr< Rawterm.NoBindings >> + <:expr< Glob_term.ImplicitBindings $l$ >> + | Glob_term.NoBindings -> + <:expr< Glob_term.NoBindings >> let mlexpr_of_binding = mlexpr_of_pair mlexpr_of_binding_kind mlexpr_of_constr @@ -473,7 +473,7 @@ and mlexpr_of_tactic : (Tacexpr.raw_tactic_expr -> MLast.expr) = function and mlexpr_of_tactic_arg = function | Tacexpr.MetaIdArg (loc,true,id) -> anti loc id | Tacexpr.MetaIdArg (loc,false,id) -> - <:expr< Tacexpr.ConstrMayEval (Rawterm.ConstrTerm $anti loc id$) >> + <:expr< Tacexpr.ConstrMayEval (Glob_term.ConstrTerm $anti loc id$) >> | Tacexpr.TacCall (loc,t,tl) -> <:expr< Tacexpr.TacCall $dloc$ $mlexpr_of_reference t$ $mlexpr_of_list mlexpr_of_tactic_arg tl$>> | Tacexpr.Tacexp t -> diff --git a/plugins/decl_mode/decl_expr.mli b/plugins/decl_mode/decl_expr.mli index 6c6dbf0f6..fa6acaeb1 100644 --- a/plugins/decl_mode/decl_expr.mli +++ b/plugins/decl_mode/decl_expr.mli @@ -93,7 +93,7 @@ type proof_pattern = pat_aliases: (Term.constr*Term.types) statement list; pat_constr: Term.constr; pat_typ: Term.types; - pat_pat: Rawterm.cases_pattern; + pat_pat: Glob_term.cases_pattern; pat_expr: Topconstr.cases_pattern_expr} type proof_instr = diff --git a/plugins/decl_mode/decl_interp.ml b/plugins/decl_mode/decl_interp.ml index d16a26550..3a3f50ac8 100644 --- a/plugins/decl_mode/decl_interp.ml +++ b/plugins/decl_mode/decl_interp.ml @@ -14,7 +14,7 @@ open Tacmach open Decl_expr open Decl_mode open Pretyping.Default -open Rawterm +open Glob_term open Term open Pp open Compat @@ -343,13 +343,13 @@ let interp_cases info sigma env params (pat:cases_pattern_expr) hyps = raw_app(dummy_loc,rind,rparams@rparams_rec@dum_args) in let pat_vars,aliases,patt = interp_pattern env pat in let inject = function - Thesis (Plain) -> Rawterm.GSort(dummy_loc,RProp Null) + Thesis (Plain) -> Glob_term.GSort(dummy_loc,RProp Null) | Thesis (For rec_occ) -> if not (List.mem rec_occ pat_vars) then errorlabstrm "suppose it is" (str "Variable " ++ Nameops.pr_id rec_occ ++ str " does not occur in pattern."); - Rawterm.GSort(dummy_loc,RProp Null) + Glob_term.GSort(dummy_loc,RProp Null) | This (c,_) -> c in let term1 = glob_constr_of_hyps inject hyps raw_prop in let loc_ids,npatt = diff --git a/plugins/decl_mode/decl_proof_instr.ml b/plugins/decl_mode/decl_proof_instr.ml index 97277ad58..cee4d7271 100644 --- a/plugins/decl_mode/decl_proof_instr.ml +++ b/plugins/decl_mode/decl_proof_instr.ml @@ -17,7 +17,7 @@ open Tacinterp open Decl_expr open Decl_mode open Decl_interp -open Rawterm +open Glob_term open Names open Nameops open Declarations diff --git a/plugins/decl_mode/decl_proof_instr.mli b/plugins/decl_mode/decl_proof_instr.mli index 94c7bac2b..0a2ab571f 100644 --- a/plugins/decl_mode/decl_proof_instr.mli +++ b/plugins/decl_mode/decl_proof_instr.mli @@ -37,20 +37,20 @@ val execute_cases : Term.constr list -> int -> Decl_mode.split_tree -> Proof_type.tactic val tree_of_pats : - identifier * (int * int) -> (Rawterm.cases_pattern*recpath) list list -> + identifier * (int * int) -> (Glob_term.cases_pattern*recpath) list list -> split_tree val add_branch : - identifier * (int * int) -> (Rawterm.cases_pattern*recpath) list list -> + identifier * (int * int) -> (Glob_term.cases_pattern*recpath) list list -> split_tree -> split_tree val append_branch : - identifier *(int * int) -> int -> (Rawterm.cases_pattern*recpath) list list -> + identifier *(int * int) -> int -> (Glob_term.cases_pattern*recpath) list list -> (Names.Idset.t * Decl_mode.split_tree) option -> (Names.Idset.t * Decl_mode.split_tree) option val append_tree : - identifier * (int * int) -> int -> (Rawterm.cases_pattern*recpath) list list -> + identifier * (int * int) -> int -> (Glob_term.cases_pattern*recpath) list list -> split_tree -> split_tree val build_dep_clause : Term.types Decl_expr.statement list -> @@ -63,7 +63,7 @@ val register_dep_subcase : Names.identifier * (int * int) -> Environ.env -> Decl_mode.per_info -> - Rawterm.cases_pattern -> Decl_mode.elim_kind -> Decl_mode.elim_kind + Glob_term.cases_pattern -> Decl_mode.elim_kind -> Decl_mode.elim_kind val thesis_for : Term.constr -> Term.constr -> Decl_mode.per_info -> Environ.env -> Term.constr diff --git a/plugins/firstorder/instances.ml b/plugins/firstorder/instances.ml index 24ec23484..881850365 100644 --- a/plugins/firstorder/instances.ml +++ b/plugins/firstorder/instances.ml @@ -12,7 +12,7 @@ open Unify open Rules open Util open Term -open Rawterm +open Glob_term open Tacmach open Tactics open Tacticals @@ -179,12 +179,12 @@ let right_instance_tac inst continue seq= [tclTHENLIST [introf; (fun gls-> - split (Rawterm.ImplicitBindings + split (Glob_term.ImplicitBindings [mkVar (Tacmach.pf_nth_hyp_id gls 1)]) gls); tclSOLVE [wrap 0 true continue (deepen seq)]]; tclTRY assumption] | Real ((0,t),_) -> - (tclTHEN (split (Rawterm.ImplicitBindings [t])) + (tclTHEN (split (Glob_term.ImplicitBindings [t])) (tclSOLVE [wrap 0 true continue (deepen seq)])) | Real ((m,t),_) -> tclFAIL 0 (Pp.str "not implemented ... yet") diff --git a/plugins/funind/functional_principles_proofs.ml b/plugins/funind/functional_principles_proofs.ml index e047f13d5..2c5118e92 100644 --- a/plugins/funind/functional_principles_proofs.ml +++ b/plugins/funind/functional_principles_proofs.ml @@ -349,9 +349,9 @@ let isLetIn t = let h_reduce_with_zeta = h_reduce - (Rawterm.Cbv - {Rawterm.all_flags - with Rawterm.rDelta = false; + (Glob_term.Cbv + {Glob_term.all_flags + with Glob_term.rDelta = false; }) @@ -963,7 +963,7 @@ let generate_equation_lemma fnames f fun_num nb_params nb_args rec_args_num = let rec_id = pf_nth_hyp_id g 1 in tclTHENSEQ [(* observe_tac "generalize_non_dep in generate_equation_lemma" *) (generalize_non_dep rec_id); - (* observe_tac "h_case" *) (h_case false (mkVar rec_id,Rawterm.NoBindings)); + (* observe_tac "h_case" *) (h_case false (mkVar rec_id,Glob_term.NoBindings)); intros_reflexivity] g ) ] @@ -1399,10 +1399,10 @@ let build_clause eqs = { Tacexpr.onhyps = Some (List.map - (fun id -> (Rawterm.all_occurrences_expr, id), Termops.InHyp) + (fun id -> (Glob_term.all_occurrences_expr, id), Termops.InHyp) eqs ); - Tacexpr.concl_occs = Rawterm.no_occurrences_expr + Tacexpr.concl_occs = Glob_term.no_occurrences_expr } let rec rewrite_eqs_in_eqs eqs = diff --git a/plugins/funind/functional_principles_types.ml b/plugins/funind/functional_principles_types.ml index 6034f19e6..c297f4965 100644 --- a/plugins/funind/functional_principles_types.ml +++ b/plugins/funind/functional_principles_types.ml @@ -501,7 +501,7 @@ let get_funs_constant mp dp = exception No_graph_found exception Found_type of int -let make_scheme (fas : (constant*Rawterm.rawsort) list) : Entries.definition_entry list = +let make_scheme (fas : (constant*Glob_term.rawsort) list) : Entries.definition_entry list = let env = Global.env () and sigma = Evd.empty in let funs = List.map fst fas in diff --git a/plugins/funind/functional_principles_types.mli b/plugins/funind/functional_principles_types.mli index fb04c6ec2..24c8359dc 100644 --- a/plugins/funind/functional_principles_types.mli +++ b/plugins/funind/functional_principles_types.mli @@ -27,8 +27,8 @@ val compute_new_princ_type_from_rel : constr array -> sorts array -> exception No_graph_found -val make_scheme : (constant*Rawterm.rawsort) list -> Entries.definition_entry list +val make_scheme : (constant*Glob_term.rawsort) list -> Entries.definition_entry list -val build_scheme : (identifier*Libnames.reference*Rawterm.rawsort) list -> unit -val build_case_scheme : (identifier*Libnames.reference*Rawterm.rawsort) -> unit +val build_scheme : (identifier*Libnames.reference*Glob_term.rawsort) list -> unit +val build_case_scheme : (identifier*Libnames.reference*Glob_term.rawsort) -> unit diff --git a/plugins/funind/g_indfun.ml4 b/plugins/funind/g_indfun.ml4 index 9873d2d5a..90f7b5970 100644 --- a/plugins/funind/g_indfun.ml4 +++ b/plugins/funind/g_indfun.ml4 @@ -19,17 +19,17 @@ open Tacticals open Constr let pr_binding prc = function - | loc, Rawterm.NamedHyp id, c -> hov 1 (Ppconstr.pr_id id ++ str " := " ++ cut () ++ prc c) - | loc, Rawterm.AnonHyp n, c -> hov 1 (int n ++ str " := " ++ cut () ++ prc c) + | loc, Glob_term.NamedHyp id, c -> hov 1 (Ppconstr.pr_id id ++ str " := " ++ cut () ++ prc c) + | loc, Glob_term.AnonHyp n, c -> hov 1 (int n ++ str " := " ++ cut () ++ prc c) let pr_bindings prc prlc = function - | Rawterm.ImplicitBindings l -> + | Glob_term.ImplicitBindings l -> brk (1,1) ++ str "with" ++ brk (1,1) ++ Util.prlist_with_sep spc prc l - | Rawterm.ExplicitBindings l -> + | Glob_term.ExplicitBindings l -> brk (1,1) ++ str "with" ++ brk (1,1) ++ Util.prlist_with_sep spc (fun b -> str"(" ++ pr_binding prlc b ++ str")") l - | Rawterm.NoBindings -> mt () + | Glob_term.NoBindings -> mt () let pr_with_bindings prc prlc (c,bl) = prc c ++ hv 0 (pr_bindings prc prlc bl) diff --git a/plugins/funind/indfun.ml b/plugins/funind/indfun.ml index b2b4145d7..6e063d3c1 100644 --- a/plugins/funind/indfun.ml +++ b/plugins/funind/indfun.ml @@ -4,7 +4,7 @@ open Term open Pp open Indfun_common open Libnames -open Rawterm +open Glob_term open Declarations let is_rec_info scheme_info = @@ -63,7 +63,7 @@ let functional_induction with_clean c princl pat = errorlabstrm "" (str "Cannot find induction principle for " ++Printer.pr_lconstr (mkConst c') ) in - (princ,Rawterm.NoBindings, Tacmach.pf_type_of g princ) + (princ,Glob_term.NoBindings, Tacmach.pf_type_of g princ) | _ -> raise (UserError("",str "functional induction must be used with a function" )) end | Some ((princ,binding)) -> @@ -101,9 +101,9 @@ let functional_induction with_clean c princl pat = (Tacmach.pf_ids_of_hyps g) in let flag = - Rawterm.Cbv - {Rawterm.all_flags - with Rawterm.rDelta = false; + Glob_term.Cbv + {Glob_term.all_flags + with Glob_term.rDelta = false; } in Tacticals.tclTHEN @@ -137,7 +137,7 @@ let interp_casted_constr_with_implicits sigma env impls c = ~allow_patvar:false ~ltacvars:([],[]) c (* - Construct a fixpoint as a Rawterm + Construct a fixpoint as a Glob_term and not as a constr *) diff --git a/plugins/funind/indfun.mli b/plugins/funind/indfun.mli index f44d12b23..e65b58086 100644 --- a/plugins/funind/indfun.mli +++ b/plugins/funind/indfun.mli @@ -4,7 +4,7 @@ open Term open Pp open Indfun_common open Libnames -open Rawterm +open Glob_term open Declarations val do_generate_principle : @@ -16,7 +16,7 @@ val do_generate_principle : val functional_induction : bool -> Term.constr -> - (Term.constr * Term.constr Rawterm.bindings) option -> + (Term.constr * Term.constr Glob_term.bindings) option -> Genarg.intro_pattern_expr Util.located option -> Proof_type.goal Tacmach.sigma -> Proof_type.goal list Evd.sigma diff --git a/plugins/funind/indfun_common.ml b/plugins/funind/indfun_common.ml index 9db361cf5..1de0f91d1 100644 --- a/plugins/funind/indfun_common.ml +++ b/plugins/funind/indfun_common.ml @@ -76,8 +76,8 @@ let chop_rlambda_n = then List.rev acc,rt else match rt with - | Rawterm.GLambda(_,name,k,t,b) -> chop_lambda_n ((name,t,false)::acc) (n-1) b - | Rawterm.GLetIn(_,name,v,b) -> chop_lambda_n ((name,v,true)::acc) (n-1) b + | Glob_term.GLambda(_,name,k,t,b) -> chop_lambda_n ((name,t,false)::acc) (n-1) b + | Glob_term.GLetIn(_,name,v,b) -> chop_lambda_n ((name,v,true)::acc) (n-1) b | _ -> raise (Util.UserError("chop_rlambda_n", str "chop_rlambda_n: Not enough Lambdas")) @@ -90,7 +90,7 @@ let chop_rprod_n = then List.rev acc,rt else match rt with - | Rawterm.GProd(_,name,k,t,b) -> chop_prod_n ((name,t)::acc) (n-1) b + | Glob_term.GProd(_,name,k,t,b) -> chop_prod_n ((name,t)::acc) (n-1) b | _ -> raise (Util.UserError("chop_rprod_n",str "chop_rprod_n: Not enough products")) in chop_prod_n [] diff --git a/plugins/funind/indfun_common.mli b/plugins/funind/indfun_common.mli index d802ecf2b..e0076735a 100644 --- a/plugins/funind/indfun_common.mli +++ b/plugins/funind/indfun_common.mli @@ -35,11 +35,11 @@ val list_union_eq : val list_add_set_eq : ('a -> 'a -> bool) -> 'a -> 'a list -> 'a list -val chop_rlambda_n : int -> Rawterm.glob_constr -> - (name*Rawterm.glob_constr*bool) list * Rawterm.glob_constr +val chop_rlambda_n : int -> Glob_term.glob_constr -> + (name*Glob_term.glob_constr*bool) list * Glob_term.glob_constr -val chop_rprod_n : int -> Rawterm.glob_constr -> - (name*Rawterm.glob_constr) list * Rawterm.glob_constr +val chop_rprod_n : int -> Glob_term.glob_constr -> + (name*Glob_term.glob_constr) list * Glob_term.glob_constr val def_of_const : Term.constr -> Term.constr val eq : Term.constr Lazy.t diff --git a/plugins/funind/invfun.ml b/plugins/funind/invfun.ml index 24382f875..4e5fb953d 100644 --- a/plugins/funind/invfun.ml +++ b/plugins/funind/invfun.ml @@ -23,17 +23,17 @@ open Hiddentac let pr_binding prc = function - | loc, Rawterm.NamedHyp id, c -> hov 1 (Ppconstr.pr_id id ++ str " := " ++ Pp.cut () ++ prc c) - | loc, Rawterm.AnonHyp n, c -> hov 1 (int n ++ str " := " ++ Pp.cut () ++ prc c) + | loc, Glob_term.NamedHyp id, c -> hov 1 (Ppconstr.pr_id id ++ str " := " ++ Pp.cut () ++ prc c) + | loc, Glob_term.AnonHyp n, c -> hov 1 (int n ++ str " := " ++ Pp.cut () ++ prc c) let pr_bindings prc prlc = function - | Rawterm.ImplicitBindings l -> + | Glob_term.ImplicitBindings l -> brk (1,1) ++ str "with" ++ brk (1,1) ++ Util.prlist_with_sep spc prc l - | Rawterm.ExplicitBindings l -> + | Glob_term.ExplicitBindings l -> brk (1,1) ++ str "with" ++ brk (1,1) ++ Util.prlist_with_sep spc (fun b -> str"(" ++ pr_binding prlc b ++ str")") l - | Rawterm.NoBindings -> mt () + | Glob_term.NoBindings -> mt () let pr_with_bindings prc prlc (c,bl) = @@ -312,7 +312,7 @@ let prove_fun_correct functional_induction funs_constr graphs_constr schemes lem | None -> (id::pre_args,pre_tac) | Some b -> (pre_args, - tclTHEN (h_reduce (Rawterm.Unfold([Rawterm.all_occurrences_expr,EvalVarRef id])) allHyps) pre_tac + tclTHEN (h_reduce (Glob_term.Unfold([Glob_term.all_occurrences_expr,EvalVarRef id])) allHyps) pre_tac ) else (pre_args,pre_tac) @@ -394,10 +394,10 @@ let prove_fun_correct functional_induction funs_constr graphs_constr schemes lem observe_tac "unfolding" pre_tac; (* $zeta$ normalizing of the conclusion *) h_reduce - (Rawterm.Cbv - { Rawterm.all_flags with - Rawterm.rDelta = false ; - Rawterm.rConst = [] + (Glob_term.Cbv + { Glob_term.all_flags with + Glob_term.rDelta = false ; + Glob_term.rConst = [] } ) onConcl; @@ -423,7 +423,7 @@ let prove_fun_correct functional_induction funs_constr graphs_constr schemes lem List.fold_left2 (fun (bindings,avoid) (x,_,_) p -> let id = Namegen.next_ident_away (Nameops.out_name x) avoid in - (dummy_loc,Rawterm.NamedHyp id,p)::bindings,id::avoid + (dummy_loc,Glob_term.NamedHyp id,p)::bindings,id::avoid ) ([],pf_ids_of_hyps g) princ_infos.params @@ -433,12 +433,12 @@ let prove_fun_correct functional_induction funs_constr graphs_constr schemes lem List.rev (fst (List.fold_left2 (fun (bindings,avoid) (x,_,_) p -> let id = Namegen.next_ident_away (Nameops.out_name x) avoid in - (dummy_loc,Rawterm.NamedHyp id,(nf_zeta p))::bindings,id::avoid) + (dummy_loc,Glob_term.NamedHyp id,(nf_zeta p))::bindings,id::avoid) ([],avoid) princ_infos.predicates (lemmas))) in - Rawterm.ExplicitBindings (params_bindings@lemmas_bindings) + Glob_term.ExplicitBindings (params_bindings@lemmas_bindings) in tclTHENSEQ [ observe_tac "intro args_names" (tclMAP h_intro args_names); @@ -516,15 +516,15 @@ and intros_with_rewrite_aux : tactic = Tauto.tauto g | Case(_,_,v,_) -> tclTHENSEQ[ - h_case false (v,Rawterm.NoBindings); + h_case false (v,Glob_term.NoBindings); intros_with_rewrite ] g | LetIn _ -> tclTHENSEQ[ h_reduce - (Rawterm.Cbv - {Rawterm.all_flags - with Rawterm.rDelta = false; + (Glob_term.Cbv + {Glob_term.all_flags + with Glob_term.rDelta = false; }) onConcl ; @@ -537,9 +537,9 @@ and intros_with_rewrite_aux : tactic = | LetIn _ -> tclTHENSEQ[ h_reduce - (Rawterm.Cbv - {Rawterm.all_flags - with Rawterm.rDelta = false; + (Glob_term.Cbv + {Glob_term.all_flags + with Glob_term.rDelta = false; }) onConcl ; @@ -553,7 +553,7 @@ let rec reflexivity_with_destruct_cases g = match kind_of_term (snd (destApp (pf_concl g))).(2) with | Case(_,_,v,_) -> tclTHENSEQ[ - h_case false (v,Rawterm.NoBindings); + h_case false (v,Glob_term.NoBindings); intros; observe_tac "reflexivity_with_destruct_cases" reflexivity_with_destruct_cases ] @@ -676,9 +676,9 @@ let prove_fun_complete funcs graphs schemes lemmas_types_infos i : tactic = Equality.rewriteLR (mkConst eq_lemma); (* Don't forget to $\zeta$ normlize the term since the principles have been $\zeta$-normalized *) h_reduce - (Rawterm.Cbv - {Rawterm.all_flags - with Rawterm.rDelta = false; + (Glob_term.Cbv + {Glob_term.all_flags + with Glob_term.rDelta = false; }) onConcl ; @@ -723,7 +723,7 @@ let prove_fun_complete funcs graphs schemes lemmas_types_infos i : tactic = (h_generalize [mkApp(applist(graph_principle,params),Array.map (fun c -> applist(c,params)) lemmas)]); h_intro graph_principle_id; observe_tac "" (tclTHEN_i - (observe_tac "elim" ((elim false (mkVar hres,Rawterm.NoBindings) (Some (mkVar graph_principle_id,Rawterm.NoBindings))))) + (observe_tac "elim" ((elim false (mkVar hres,Glob_term.NoBindings) (Some (mkVar graph_principle_id,Glob_term.NoBindings))))) (fun i g -> observe_tac "prove_branche" (prove_branche i) g )) ] g @@ -774,7 +774,7 @@ let derive_correctness make_scheme functional_induction (funs: constant list) (g (fun entry -> (entry.Entries.const_entry_body, Option.get entry.Entries.const_entry_type ) ) - (make_scheme (array_map_to_list (fun const -> const,Rawterm.RType None) funs)) + (make_scheme (array_map_to_list (fun const -> const,Glob_term.RType None) funs)) ) in let proving_tac = @@ -945,7 +945,7 @@ let functional_inversion kn hid fconst f_correct : tactic = h_generalize [applist(f_correct,(Array.to_list f_args)@[res;mkVar hid])]; thin [hid]; h_intro hid; - Inv.inv FullInversion None (Rawterm.NamedHyp hid); + Inv.inv FullInversion None (Glob_term.NamedHyp hid); (fun g -> let new_ids = List.filter (fun id -> not (Idset.mem id old_ids)) (pf_ids_of_hyps g) in tclMAP (revert_graph kn pre_tac) (hid::new_ids) g diff --git a/plugins/funind/merge.ml b/plugins/funind/merge.ml index ed8cb9cb6..f757bafcb 100644 --- a/plugins/funind/merge.ml +++ b/plugins/funind/merge.ml @@ -20,7 +20,7 @@ open Term open Termops open Declarations open Environ -open Rawterm +open Glob_term open Rawtermops (** {1 Utilities} *) diff --git a/plugins/funind/rawterm_to_relation.ml b/plugins/funind/rawterm_to_relation.ml index 7b67e20f3..061600795 100644 --- a/plugins/funind/rawterm_to_relation.ml +++ b/plugins/funind/rawterm_to_relation.ml @@ -2,7 +2,7 @@ open Printer open Pp open Names open Term -open Rawterm +open Glob_term open Libnames open Indfun_common open Util @@ -701,7 +701,7 @@ let rec build_entry_lc env funnames avoid rt : glob_constr build_entry_return = | GDynamic _ -> error "Not handled GDynamic" and build_entry_lc_from_case env funname make_discr (el:tomatch_tuples) - (brl:Rawterm.cases_clauses) avoid : + (brl:Glob_term.cases_clauses) avoid : glob_constr build_entry_return = match el with | [] -> assert false (* this case correspond to match <nothing> with .... !*) @@ -1162,7 +1162,7 @@ and compute_cst_params_from_app acc (params,rtl) = compute_cst_params_from_app (param::acc) (params',rtl') | _ -> List.rev acc -let compute_params_name relnames (args : (Names.name * Rawterm.glob_constr * bool) list array) csts = +let compute_params_name relnames (args : (Names.name * Glob_term.glob_constr * bool) list array) csts = let rels_params = Array.mapi (fun i args -> @@ -1233,7 +1233,7 @@ let do_build_inductive let resa = Array.map (build_entry_lc env funnames_as_set []) rta in let env_with_graphs = let rel_arity i funargs = (* Reduilding arities (with parameters) *) - let rel_first_args :(Names.name * Rawterm.glob_constr * bool ) list = + let rel_first_args :(Names.name * Glob_term.glob_constr * bool ) list = funargs in List.fold_right @@ -1299,7 +1299,7 @@ let do_build_inductive rel_constructors in let rel_arity i funargs = (* Reduilding arities (with parameters) *) - let rel_first_args :(Names.name * Rawterm.glob_constr * bool ) list = + let rel_first_args :(Names.name * Glob_term.glob_constr * bool ) list = (snd (list_chop nrel_params funargs)) in List.fold_right diff --git a/plugins/funind/rawterm_to_relation.mli b/plugins/funind/rawterm_to_relation.mli index 772e422f8..5c91292ba 100644 --- a/plugins/funind/rawterm_to_relation.mli +++ b/plugins/funind/rawterm_to_relation.mli @@ -9,8 +9,8 @@ val build_inductive : Names.identifier list -> (* The list of function name *) - (Names.name*Rawterm.glob_constr*bool) list list -> (* The list of function args *) + (Names.name*Glob_term.glob_constr*bool) list list -> (* The list of function args *) Topconstr.constr_expr list -> (* The list of function returned type *) - Rawterm.glob_constr list -> (* the list of body *) + Glob_term.glob_constr list -> (* the list of body *) unit diff --git a/plugins/funind/rawtermops.ml b/plugins/funind/rawtermops.ml index f372fb017..0cf91f38c 100644 --- a/plugins/funind/rawtermops.ml +++ b/plugins/funind/rawtermops.ml @@ -1,5 +1,5 @@ open Pp -open Rawterm +open Glob_term open Util open Names (* Ocaml 3.06 Map.S does not handle is_empty *) diff --git a/plugins/funind/rawtermops.mli b/plugins/funind/rawtermops.mli index 9e872c236..b6c407a24 100644 --- a/plugins/funind/rawtermops.mli +++ b/plugins/funind/rawtermops.mli @@ -1,4 +1,4 @@ -open Rawterm +open Glob_term (* Ocaml 3.06 Map.S does not handle is_empty *) val idmap_is_empty : 'a Names.Idmap.t -> bool @@ -73,8 +73,8 @@ val change_vars : Names.identifier Names.Idmap.t -> glob_constr -> glob_constr *) val alpha_pat : Names.Idmap.key list -> - Rawterm.cases_pattern -> - Rawterm.cases_pattern * Names.Idmap.key list * + Glob_term.cases_pattern -> + Glob_term.cases_pattern * Names.Idmap.key list * Names.identifier Names.Idmap.t (* [alpha_rt avoid rt] alpha convert [rt] s.t. the result repects barendregt @@ -84,16 +84,16 @@ val alpha_rt : Names.identifier list -> glob_constr -> glob_constr (* same as alpha_rt but for case branches *) val alpha_br : Names.identifier list -> - Util.loc * Names.identifier list * Rawterm.cases_pattern list * - Rawterm.glob_constr -> - Util.loc * Names.identifier list * Rawterm.cases_pattern list * - Rawterm.glob_constr + Util.loc * Names.identifier list * Glob_term.cases_pattern list * + Glob_term.glob_constr -> + Util.loc * Names.identifier list * Glob_term.cases_pattern list * + Glob_term.glob_constr (* Reduction function *) val replace_var_by_term : Names.identifier -> - Rawterm.glob_constr -> Rawterm.glob_constr -> Rawterm.glob_constr + Glob_term.glob_constr -> Glob_term.glob_constr -> Glob_term.glob_constr @@ -120,7 +120,7 @@ val ids_of_rawterm: glob_constr -> Names.Idset.t (* removing let_in construction in a rawterm *) -val zeta_normalize : Rawterm.glob_constr -> Rawterm.glob_constr +val zeta_normalize : Glob_term.glob_constr -> Glob_term.glob_constr val expand_as : glob_constr -> glob_constr diff --git a/plugins/funind/recdef.ml b/plugins/funind/recdef.ml index 1b43d4045..3ab9d58d5 100644 --- a/plugins/funind/recdef.ml +++ b/plugins/funind/recdef.ml @@ -33,7 +33,7 @@ open Proof_type open Vernacinterp open Pfedit open Topconstr -open Rawterm +open Glob_term open Pretyping open Pretyping.Default open Safe_typing diff --git a/plugins/micromega/g_micromega.ml4 b/plugins/micromega/g_micromega.ml4 index 68dc7fe0b..20fcd9720 100644 --- a/plugins/micromega/g_micromega.ml4 +++ b/plugins/micromega/g_micromega.ml4 @@ -19,7 +19,7 @@ open Quote open Ring open Mutils -open Rawterm +open Glob_term open Util let out_arg = function diff --git a/plugins/nsatz/nsatz.ml4 b/plugins/nsatz/nsatz.ml4 index b235b5821..2b5a3e7c8 100644 --- a/plugins/nsatz/nsatz.ml4 +++ b/plugins/nsatz/nsatz.ml4 @@ -16,7 +16,7 @@ open Closure open Environ open Libnames open Tactics -open Rawterm +open Glob_term open Tacticals open Tacexpr open Pcoq diff --git a/plugins/omega/coq_omega.ml b/plugins/omega/coq_omega.ml index 6bdfea4ad..83ecf72ee 100644 --- a/plugins/omega/coq_omega.ml +++ b/plugins/omega/coq_omega.ml @@ -125,7 +125,7 @@ let intern_id,unintern_id = let mk_then = tclTHENLIST -let exists_tac c = constructor_tac false (Some 1) 1 (Rawterm.ImplicitBindings [c]) +let exists_tac c = constructor_tac false (Some 1) 1 (Glob_term.ImplicitBindings [c]) let generalize_tac t = generalize_time (generalize t) let elim t = elim_time (simplest_elim t) diff --git a/plugins/setoid_ring/newring.ml4 b/plugins/setoid_ring/newring.ml4 index 112a13e53..9a79f2878 100644 --- a/plugins/setoid_ring/newring.ml4 +++ b/plugins/setoid_ring/newring.ml4 @@ -16,7 +16,7 @@ open Closure open Environ open Libnames open Tactics -open Rawterm +open Glob_term open Tacticals open Tacexpr open Pcoq diff --git a/plugins/subtac/g_subtac.ml4 b/plugins/subtac/g_subtac.ml4 index 6326ced8c..c42f13b04 100644 --- a/plugins/subtac/g_subtac.ml4 +++ b/plugins/subtac/g_subtac.ml4 @@ -40,7 +40,7 @@ struct let subtac_withtac : Tacexpr.raw_tactic_expr option Gram.entry = gec "subtac_withtac" end -open Rawterm +open Glob_term open SubtacGram open Util open Pcoq diff --git a/plugins/subtac/subtac.ml b/plugins/subtac/subtac.ml index 0ea2290db..e614085e4 100644 --- a/plugins/subtac/subtac.ml +++ b/plugins/subtac/subtac.ml @@ -26,7 +26,7 @@ open List open Recordops open Evarutil open Pretype_errors -open Rawterm +open Glob_term open Evarconv open Pattern open Vernacexpr diff --git a/plugins/subtac/subtac_cases.ml b/plugins/subtac/subtac_cases.ml index 5ef6f0f88..4dfdc5875 100644 --- a/plugins/subtac/subtac_cases.ml +++ b/plugins/subtac/subtac_cases.ml @@ -20,7 +20,7 @@ open Sign open Reductionops open Typeops open Type_errors -open Rawterm +open Glob_term open Retyping open Pretype_errors open Evarutil diff --git a/plugins/subtac/subtac_cases.mli b/plugins/subtac/subtac_cases.mli index 253eacd36..77537d33a 100644 --- a/plugins/subtac/subtac_cases.mli +++ b/plugins/subtac/subtac_cases.mli @@ -13,7 +13,7 @@ open Term open Evd open Environ open Inductiveops -open Rawterm +open Glob_term open Evarutil (*i*) diff --git a/plugins/subtac/subtac_classes.ml b/plugins/subtac/subtac_classes.ml index 88f88b7f2..0d5f7b86e 100644 --- a/plugins/subtac/subtac_classes.ml +++ b/plugins/subtac/subtac_classes.ml @@ -10,7 +10,7 @@ open Pretyping open Evd open Environ open Term -open Rawterm +open Glob_term open Topconstr open Names open Libnames diff --git a/plugins/subtac/subtac_coercion.ml b/plugins/subtac/subtac_coercion.ml index a1159dcaa..a09fa3dcc 100644 --- a/plugins/subtac/subtac_coercion.ml +++ b/plugins/subtac/subtac_coercion.ml @@ -327,8 +327,8 @@ module Coercion = struct let apply_pattern_coercion loc pat p = List.fold_left (fun pat (co,n) -> - let f i = if i<n then Rawterm.PatVar (loc, Anonymous) else pat in - Rawterm.PatCstr (loc, co, list_tabulate f (n+1), Anonymous)) + let f i = if i<n then Glob_term.PatVar (loc, Anonymous) else pat in + Glob_term.PatCstr (loc, co, list_tabulate f (n+1), Anonymous)) pat p (* raise Not_found if no coercion found *) diff --git a/plugins/subtac/subtac_command.ml b/plugins/subtac/subtac_command.ml index 24fdd679b..794143de4 100644 --- a/plugins/subtac/subtac_command.ml +++ b/plugins/subtac/subtac_command.ml @@ -6,7 +6,7 @@ open Libobject open Pattern open Matching open Pp -open Rawterm +open Glob_term open Sign open Tacred open Util diff --git a/plugins/subtac/subtac_pretyping.ml b/plugins/subtac/subtac_pretyping.ml index 09cc17328..c7924261a 100644 --- a/plugins/subtac/subtac_pretyping.ml +++ b/plugins/subtac/subtac_pretyping.ml @@ -24,7 +24,7 @@ open List open Recordops open Evarutil open Pretype_errors -open Rawterm +open Glob_term open Evarconv open Pattern @@ -81,9 +81,9 @@ let find_with_index x l = open Vernacexpr -let coqintern_constr evd env : Topconstr.constr_expr -> Rawterm.glob_constr = +let coqintern_constr evd env : Topconstr.constr_expr -> Glob_term.glob_constr = Constrintern.intern_constr evd env -let coqintern_type evd env : Topconstr.constr_expr -> Rawterm.glob_constr = +let coqintern_type evd env : Topconstr.constr_expr -> Glob_term.glob_constr = Constrintern.intern_type evd env let env_with_binders env isevars l = diff --git a/plugins/subtac/subtac_pretyping.mli b/plugins/subtac/subtac_pretyping.mli index 2b0c8fda2..fa767790d 100644 --- a/plugins/subtac/subtac_pretyping.mli +++ b/plugins/subtac/subtac_pretyping.mli @@ -13,7 +13,7 @@ module Pretyping : Pretyping.S val interp : Environ.env -> Evd.evar_map ref -> - Rawterm.glob_constr -> + Glob_term.glob_constr -> Evarutil.type_constraint -> Term.constr * Term.constr val subtac_process : ?is_type:bool -> env -> evar_map ref -> identifier -> local_binder list -> diff --git a/plugins/subtac/subtac_pretyping_F.ml b/plugins/subtac/subtac_pretyping_F.ml index debd4f053..b1c4101ce 100644 --- a/plugins/subtac/subtac_pretyping_F.ml +++ b/plugins/subtac/subtac_pretyping_F.ml @@ -24,7 +24,7 @@ open List open Recordops open Evarutil open Pretype_errors -open Rawterm +open Glob_term open Evarconv open Pattern open Pretyping diff --git a/plugins/subtac/subtac_utils.ml b/plugins/subtac/subtac_utils.ml index 43b55ca95..48ff28aee 100644 --- a/plugins/subtac/subtac_utils.ml +++ b/plugins/subtac/subtac_utils.ml @@ -249,7 +249,7 @@ let build_dependent_sum l = ([intros; (tclTHENSEQ [constructor_tac false (Some 1) 1 - (Rawterm.ImplicitBindings [mkVar n]); + (Glob_term.ImplicitBindings [mkVar n]); cont]); ]))) in @@ -352,7 +352,7 @@ let destruct_ex ext ex = | _ -> [acc] in aux ex ext -open Rawterm +open Glob_term let id_of_name = function Name n -> n diff --git a/plugins/subtac/subtac_utils.mli b/plugins/subtac/subtac_utils.mli index 659a67781..8c983377a 100644 --- a/plugins/subtac/subtac_utils.mli +++ b/plugins/subtac/subtac_utils.mli @@ -6,7 +6,7 @@ open Pp open Evd open Decl_kinds open Topconstr -open Rawterm +open Glob_term open Util open Evarutil open Names diff --git a/plugins/syntax/ascii_syntax.ml b/plugins/syntax/ascii_syntax.ml index 50498f0f4..bd2285bb3 100644 --- a/plugins/syntax/ascii_syntax.ml +++ b/plugins/syntax/ascii_syntax.ml @@ -10,7 +10,7 @@ open Pp open Util open Names open Pcoq -open Rawterm +open Glob_term open Topconstr open Libnames open Coqlib diff --git a/plugins/syntax/nat_syntax.ml b/plugins/syntax/nat_syntax.ml index 3d8860be4..446ae5225 100644 --- a/plugins/syntax/nat_syntax.ml +++ b/plugins/syntax/nat_syntax.ml @@ -14,7 +14,7 @@ open Pp open Util open Names open Coqlib -open Rawterm +open Glob_term open Libnames open Bigint open Coqlib diff --git a/plugins/syntax/numbers_syntax.ml b/plugins/syntax/numbers_syntax.ml index 892a5595a..19a3c899f 100644 --- a/plugins/syntax/numbers_syntax.ml +++ b/plugins/syntax/numbers_syntax.ml @@ -10,7 +10,7 @@ open Bigint open Libnames -open Rawterm +open Glob_term (*** Constants for locating int31 / bigN / bigZ / bigQ constructors ***) diff --git a/plugins/syntax/r_syntax.ml b/plugins/syntax/r_syntax.ml index fc953e5e5..b9c0bcd6f 100644 --- a/plugins/syntax/r_syntax.ml +++ b/plugins/syntax/r_syntax.ml @@ -20,7 +20,7 @@ exception Non_closed_number (**********************************************************************) open Libnames -open Rawterm +open Glob_term open Bigint let make_dir l = make_dirpath (List.map id_of_string (List.rev l)) diff --git a/plugins/syntax/string_syntax.ml b/plugins/syntax/string_syntax.ml index 61643881e..d670f6026 100644 --- a/plugins/syntax/string_syntax.ml +++ b/plugins/syntax/string_syntax.ml @@ -13,7 +13,7 @@ open Pcoq open Libnames open Topconstr open Ascii_syntax -open Rawterm +open Glob_term open Coqlib exception Non_closed_string diff --git a/plugins/syntax/z_syntax.ml b/plugins/syntax/z_syntax.ml index 81588bced..cf0253d1f 100644 --- a/plugins/syntax/z_syntax.ml +++ b/plugins/syntax/z_syntax.ml @@ -21,7 +21,7 @@ exception Non_closed_number (**********************************************************************) open Libnames -open Rawterm +open Glob_term let make_dir l = make_dirpath (List.map id_of_string (List.rev l)) let positive_module = ["Coq";"PArith";"BinPos"] let make_path dir id = Libnames.make_path (make_dir dir) (id_of_string id) diff --git a/plugins/xml/doubleTypeInference.ml b/plugins/xml/doubleTypeInference.ml index c8bb308f5..a21a919ad 100644 --- a/plugins/xml/doubleTypeInference.ml +++ b/plugins/xml/doubleTypeInference.ml @@ -27,7 +27,7 @@ let cprop = ;; let whd_betadeltaiotacprop env _evar_map ty = - let module R = Rawterm in + let module R = Glob_term in let module C = Closure in let module CR = C.RedFlags in (*** CProp is made Opaque ***) diff --git a/pretyping/cases.ml b/pretyping/cases.ml index 5115b3e3b..6abcd0314 100644 --- a/pretyping/cases.ml +++ b/pretyping/cases.ml @@ -20,7 +20,7 @@ open Sign open Reductionops open Typeops open Type_errors -open Rawterm +open Glob_term open Retyping open Pretype_errors open Evarutil diff --git a/pretyping/cases.mli b/pretyping/cases.mli index 015b386a5..1ff5b883e 100644 --- a/pretyping/cases.mli +++ b/pretyping/cases.mli @@ -12,7 +12,7 @@ open Term open Evd open Environ open Inductiveops -open Rawterm +open Glob_term open Evarutil (** {5 Compilation of pattern-matching } *) diff --git a/pretyping/classops.ml b/pretyping/classops.ml index 2d2677ee0..8205a6b2e 100644 --- a/pretyping/classops.ml +++ b/pretyping/classops.ml @@ -17,7 +17,7 @@ open Libobject open Library open Term open Termops -open Rawterm +open Glob_term open Decl_kinds open Mod_subst diff --git a/pretyping/coercion.ml b/pretyping/coercion.ml index f10fcbc2c..5503a147a 100644 --- a/pretyping/coercion.ml +++ b/pretyping/coercion.ml @@ -73,7 +73,7 @@ module type S = sig pattern [pat] typed in [ind1] into a pattern typed in [ind2]; raises [Not_found] if no coercion found *) val inh_pattern_coerce_to : - loc -> Rawterm.cases_pattern -> inductive -> inductive -> Rawterm.cases_pattern + loc -> Glob_term.cases_pattern -> inductive -> inductive -> Glob_term.cases_pattern end module Default = struct @@ -99,8 +99,8 @@ module Default = struct let apply_pattern_coercion loc pat p = List.fold_left (fun pat (co,n) -> - let f i = if i<n then Rawterm.PatVar (loc, Anonymous) else pat in - Rawterm.PatCstr (loc, co, list_tabulate f (n+1), Anonymous)) + let f i = if i<n then Glob_term.PatVar (loc, Anonymous) else pat in + Glob_term.PatCstr (loc, co, list_tabulate f (n+1), Anonymous)) pat p (* raise Not_found if no coercion found *) diff --git a/pretyping/coercion.mli b/pretyping/coercion.mli index 24c43e051..5d814b294 100644 --- a/pretyping/coercion.mli +++ b/pretyping/coercion.mli @@ -13,7 +13,7 @@ open Term open Sign open Environ open Evarutil -open Rawterm +open Glob_term module type S = sig (** {6 Coercions. } *) diff --git a/pretyping/detyping.ml b/pretyping/detyping.ml index 7469111bf..4ff4cd333 100644 --- a/pretyping/detyping.ml +++ b/pretyping/detyping.ml @@ -16,7 +16,7 @@ open Inductive open Inductiveops open Environ open Sign -open Rawterm +open Glob_term open Nameops open Termops open Namegen diff --git a/pretyping/detyping.mli b/pretyping/detyping.mli index e2644592c..fd16c0013 100644 --- a/pretyping/detyping.mli +++ b/pretyping/detyping.mli @@ -11,7 +11,7 @@ open Names open Term open Sign open Environ -open Rawterm +open Glob_term open Termops open Mod_subst diff --git a/pretyping/evarutil.ml b/pretyping/evarutil.ml index 80fb4d94e..ae3f64b9c 100644 --- a/pretyping/evarutil.ml +++ b/pretyping/evarutil.ml @@ -1401,7 +1401,7 @@ let check_evars env initial_sigma sigma c = | _ -> iter_constr proc_rec c in proc_rec c -open Rawterm +open Glob_term (* Operations on value/type constraints *) diff --git a/pretyping/evarutil.mli b/pretyping/evarutil.mli index 3b95784dd..35932bb8e 100644 --- a/pretyping/evarutil.mli +++ b/pretyping/evarutil.mli @@ -8,7 +8,7 @@ open Util open Names -open Rawterm +open Glob_term open Term open Sign open Evd diff --git a/pretyping/rawterm.ml b/pretyping/glob_term.ml index deba9a257..deba9a257 100644 --- a/pretyping/rawterm.ml +++ b/pretyping/glob_term.ml diff --git a/pretyping/rawterm.mli b/pretyping/glob_term.mli index 95305d58c..95305d58c 100644 --- a/pretyping/rawterm.mli +++ b/pretyping/glob_term.mli diff --git a/pretyping/matching.ml b/pretyping/matching.ml index b971db135..fc56f31d3 100644 --- a/pretyping/matching.ml +++ b/pretyping/matching.ml @@ -14,7 +14,7 @@ open Nameops open Termops open Reductionops open Term -open Rawterm +open Glob_term open Sign open Environ open Pattern diff --git a/pretyping/pattern.ml b/pretyping/pattern.ml index 2217074fe..19c5d156a 100644 --- a/pretyping/pattern.ml +++ b/pretyping/pattern.ml @@ -11,7 +11,7 @@ open Names open Libnames open Nameops open Term -open Rawterm +open Glob_term open Environ open Nametab open Pp diff --git a/pretyping/pattern.mli b/pretyping/pattern.mli index a739a2888..b25637de9 100644 --- a/pretyping/pattern.mli +++ b/pretyping/pattern.mli @@ -16,7 +16,7 @@ open Term open Environ open Libnames open Nametab -open Rawterm +open Glob_term open Mod_subst (** {5 Maps of pattern variables} *) diff --git a/pretyping/pretype_errors.ml b/pretyping/pretype_errors.ml index cd2ed76c1..b33157414 100644 --- a/pretyping/pretype_errors.ml +++ b/pretyping/pretype_errors.ml @@ -15,7 +15,7 @@ open Termops open Namegen open Environ open Type_errors -open Rawterm +open Glob_term open Inductiveops type pretype_error = diff --git a/pretyping/pretype_errors.mli b/pretyping/pretype_errors.mli index cdf6b523c..11722bee2 100644 --- a/pretyping/pretype_errors.mli +++ b/pretyping/pretype_errors.mli @@ -12,7 +12,7 @@ open Names open Term open Sign open Environ -open Rawterm +open Glob_term open Inductiveops (** {6 The type of errors raised by the pretyper } *) diff --git a/pretyping/pretyping.ml b/pretyping/pretyping.ml index bc80296d5..baa783d0c 100644 --- a/pretyping/pretyping.ml +++ b/pretyping/pretyping.ml @@ -40,7 +40,7 @@ open List open Recordops open Evarutil open Pretype_errors -open Rawterm +open Glob_term open Evarconv open Pattern diff --git a/pretyping/pretyping.mli b/pretyping/pretyping.mli index 8c0270743..70e1a22fb 100644 --- a/pretyping/pretyping.mli +++ b/pretyping/pretyping.mli @@ -17,7 +17,7 @@ open Sign open Term open Environ open Evd -open Rawterm +open Glob_term open Evarutil (** An auxiliary function for searching for fixpoint guard indexes *) diff --git a/pretyping/pretyping.mllib b/pretyping/pretyping.mllib index 6aa00c5f2..6e2c0a761 100644 --- a/pretyping/pretyping.mllib +++ b/pretyping/pretyping.mllib @@ -12,7 +12,7 @@ Term_dnet Recordops Evarconv Typing -Rawterm +Glob_term Pattern Matching Tacred diff --git a/pretyping/tacred.ml b/pretyping/tacred.ml index 90e0683c0..99776367b 100644 --- a/pretyping/tacred.ml +++ b/pretyping/tacred.ml @@ -20,7 +20,7 @@ open Environ open Closure open Reductionops open Cbv -open Rawterm +open Glob_term open Pattern open Matching diff --git a/pretyping/tacred.mli b/pretyping/tacred.mli index 733f38382..d713eae42 100644 --- a/pretyping/tacred.mli +++ b/pretyping/tacred.mli @@ -12,7 +12,7 @@ open Environ open Evd open Reductionops open Closure -open Rawterm +open Glob_term open Termops open Pattern diff --git a/pretyping/unification.ml b/pretyping/unification.ml index 6c17567c3..fd287f3af 100644 --- a/pretyping/unification.ml +++ b/pretyping/unification.ml @@ -18,7 +18,7 @@ open Environ open Evd open Reduction open Reductionops -open Rawterm +open Glob_term open Pattern open Evarutil open Pretype_errors diff --git a/proofs/clenv.ml b/proofs/clenv.ml index 4fc6c5b35..e00e278cd 100644 --- a/proofs/clenv.ml +++ b/proofs/clenv.ml @@ -18,7 +18,7 @@ open Environ open Evd open Reduction open Reductionops -open Rawterm +open Glob_term open Pattern open Tacred open Pretype_errors diff --git a/proofs/clenv.mli b/proofs/clenv.mli index 363cf423b..af51e6716 100644 --- a/proofs/clenv.mli +++ b/proofs/clenv.mli @@ -14,7 +14,7 @@ open Environ open Evd open Evarutil open Mod_subst -open Rawterm +open Glob_term open Unification (** {6 The Type of Constructions clausale environments.} *) diff --git a/proofs/clenvtac.ml b/proofs/clenvtac.ml index 90c2335d6..76f3856e3 100644 --- a/proofs/clenvtac.ml +++ b/proofs/clenvtac.ml @@ -22,7 +22,7 @@ open Logic open Reduction open Reductionops open Tacmach -open Rawterm +open Glob_term open Pattern open Tacexpr open Clenv diff --git a/proofs/evar_refiner.ml b/proofs/evar_refiner.ml index 43c7e6e5a..fdd510831 100644 --- a/proofs/evar_refiner.ml +++ b/proofs/evar_refiner.ml @@ -43,7 +43,7 @@ let w_refine (evk,evi) (ltac_var,rawc) sigma = try Pretyping.Default.understand_ltac true sigma env ltac_var (Pretyping.OfType (Some evi.evar_concl)) rawc with _ -> - let loc = Rawterm.loc_of_glob_constr rawc in + let loc = Glob_term.loc_of_glob_constr rawc in user_err_loc (loc,"",Pp.str ("Instance is not well-typed in the environment of " ^ string_of_existential evk)) diff --git a/proofs/evar_refiner.mli b/proofs/evar_refiner.mli index b800d0d66..8e7c07135 100644 --- a/proofs/evar_refiner.mli +++ b/proofs/evar_refiner.mli @@ -12,7 +12,7 @@ open Environ open Evd open Refiner open Pretyping -open Rawterm +open Glob_term (** Refinement of existential variables. *) diff --git a/proofs/goal.mli b/proofs/goal.mli index 3d9fcc5a2..fbf7e78e2 100644 --- a/proofs/goal.mli +++ b/proofs/goal.mli @@ -73,7 +73,7 @@ module Refinable : sig context of a term, the remaining evars are registered to the handle. It is the main component of the toplevel refine tactic.*) val constr_of_raw : - handle -> bool -> bool -> Rawterm.glob_constr -> Term.constr sensitive + handle -> bool -> bool -> Glob_term.glob_constr -> Term.constr sensitive end diff --git a/proofs/proof_type.ml b/proofs/proof_type.ml index ebb6db213..e256794a7 100644 --- a/proofs/proof_type.ml +++ b/proofs/proof_type.ml @@ -15,7 +15,7 @@ open Term open Util open Tacexpr (* open Decl_expr *) -open Rawterm +open Glob_term open Genarg open Nametab open Pattern diff --git a/proofs/proof_type.mli b/proofs/proof_type.mli index cf73e0dca..2b0a10ba3 100644 --- a/proofs/proof_type.mli +++ b/proofs/proof_type.mli @@ -13,7 +13,7 @@ open Libnames open Term open Util open Tacexpr -open Rawterm +open Glob_term open Genarg open Nametab open Pattern diff --git a/proofs/redexpr.ml b/proofs/redexpr.ml index d150f2a38..69ef4598d 100644 --- a/proofs/redexpr.ml +++ b/proofs/redexpr.ml @@ -12,7 +12,7 @@ open Names open Term open Declarations open Libnames -open Rawterm +open Glob_term open Pattern open Reductionops open Tacred diff --git a/proofs/redexpr.mli b/proofs/redexpr.mli index 59b7bbd6e..ae82153d2 100644 --- a/proofs/redexpr.mli +++ b/proofs/redexpr.mli @@ -10,7 +10,7 @@ open Names open Term open Closure open Pattern -open Rawterm +open Glob_term open Reductionops open Termops diff --git a/proofs/tacexpr.ml b/proofs/tacexpr.ml index b9e22ca05..428c67475 100644 --- a/proofs/tacexpr.ml +++ b/proofs/tacexpr.ml @@ -10,7 +10,7 @@ open Names open Topconstr open Libnames open Nametab -open Rawterm +open Glob_term open Util open Genarg open Pattern diff --git a/proofs/tacmach.ml b/proofs/tacmach.ml index 116526d61..5bfdba8a4 100644 --- a/proofs/tacmach.ml +++ b/proofs/tacmach.ml @@ -202,7 +202,7 @@ let rename_hyp l = with_check (rename_hyp_no_check l) open Pp open Tacexpr -open Rawterm +open Glob_term let db_pr_goal sigma g = let env = Goal.V82.env sigma g in diff --git a/proofs/tacmach.mli b/proofs/tacmach.mli index cb26d7be6..884a03070 100644 --- a/proofs/tacmach.mli +++ b/proofs/tacmach.mli @@ -16,7 +16,7 @@ open Proof_type open Refiner open Redexpr open Tacexpr -open Rawterm +open Glob_term open Pattern (** Operations for handling terms under a local typing context. *) diff --git a/tactics/auto.ml b/tactics/auto.ml index 440f92b7f..8a05736ca 100644 --- a/tactics/auto.ml +++ b/tactics/auto.ml @@ -25,7 +25,7 @@ open Matching open Tacmach open Proof_type open Pfedit -open Rawterm +open Glob_term open Evar_refiner open Tacred open Tactics diff --git a/tactics/auto.mli b/tactics/auto.mli index fa6f1d9ca..73249d43a 100644 --- a/tactics/auto.mli +++ b/tactics/auto.mli @@ -30,7 +30,7 @@ type auto_tactic = | Unfold_nth of evaluable_global_reference (** Hint Unfold *) | Extern of Tacexpr.glob_tactic_expr (** Hint Extern *) -open Rawterm +open Glob_term type pri_auto_tactic = { pri : int; (** A number between 0 and 4, 4 = lower priority *) diff --git a/tactics/autorewrite.ml b/tactics/autorewrite.ml index fb5b2f527..73f8fde29 100644 --- a/tactics/autorewrite.ml +++ b/tactics/autorewrite.ml @@ -17,7 +17,7 @@ open Tactics open Term open Termops open Util -open Rawterm +open Glob_term open Vernacinterp open Tacexpr open Mod_subst diff --git a/tactics/class_tactics.ml4 b/tactics/class_tactics.ml4 index b42df0109..1cf41a70a 100644 --- a/tactics/class_tactics.ml4 +++ b/tactics/class_tactics.ml4 @@ -25,7 +25,7 @@ open Tactics open Pattern open Clenv open Auto -open Rawterm +open Glob_term open Hiddentac open Typeclasses open Typeclasses_errors diff --git a/tactics/contradiction.ml b/tactics/contradiction.ml index 0433df28d..a3d43623e 100644 --- a/tactics/contradiction.ml +++ b/tactics/contradiction.ml @@ -15,7 +15,7 @@ open Tacticals open Tactics open Coqlib open Reductionops -open Rawterm +open Glob_term (* Absurd *) diff --git a/tactics/contradiction.mli b/tactics/contradiction.mli index c02d691a0..b77b2721a 100644 --- a/tactics/contradiction.mli +++ b/tactics/contradiction.mli @@ -9,7 +9,7 @@ open Names open Term open Proof_type -open Rawterm +open Glob_term open Genarg val absurd : constr -> tactic diff --git a/tactics/dhyp.ml b/tactics/dhyp.ml index e1e04c8ef..f9c316955 100644 --- a/tactics/dhyp.ml +++ b/tactics/dhyp.ml @@ -116,7 +116,7 @@ open Term open Environ open Reduction open Proof_type -open Rawterm +open Glob_term open Tacmach open Refiner open Tactics diff --git a/tactics/dhyp.mli b/tactics/dhyp.mli index 47c7214f1..1bdeed6aa 100644 --- a/tactics/dhyp.mli +++ b/tactics/dhyp.mli @@ -24,5 +24,5 @@ val h_auto_tdb : int option -> tactic val add_destructor_hint : Vernacexpr.locality_flag -> identifier -> (bool,unit) Tacexpr.location -> - Rawterm.patvar list * Pattern.constr_pattern -> int -> + Glob_term.patvar list * Pattern.constr_pattern -> int -> glob_tactic_expr -> unit diff --git a/tactics/eauto.ml4 b/tactics/eauto.ml4 index 6f4d90ab4..ed8da10a0 100644 --- a/tactics/eauto.ml4 +++ b/tactics/eauto.ml4 @@ -25,7 +25,7 @@ open Tactics open Pattern open Clenv open Auto -open Rawterm +open Glob_term open Hiddentac let eauto_unif_flags = { auto_unif_flags with Unification.modulo_delta = full_transparent_state } diff --git a/tactics/elim.mli b/tactics/elim.mli index fcf469e2c..48a7ca68c 100644 --- a/tactics/elim.mli +++ b/tactics/elim.mli @@ -30,5 +30,5 @@ val h_decompose : inductive list -> constr -> tactic val h_decompose_or : constr -> tactic val h_decompose_and : constr -> tactic -val double_ind : Rawterm.quantified_hypothesis -> Rawterm.quantified_hypothesis -> tactic -val h_double_induction : Rawterm.quantified_hypothesis -> Rawterm.quantified_hypothesis->tactic +val double_ind : Glob_term.quantified_hypothesis -> Glob_term.quantified_hypothesis -> tactic +val h_double_induction : Glob_term.quantified_hypothesis -> Glob_term.quantified_hypothesis->tactic diff --git a/tactics/equality.ml b/tactics/equality.ml index 0144fbb34..a2e76cd9e 100644 --- a/tactics/equality.ml +++ b/tactics/equality.ml @@ -33,7 +33,7 @@ open Tacexpr open Tacticals open Tactics open Tacred -open Rawterm +open Glob_term open Coqlib open Vernacexpr open Declarations diff --git a/tactics/equality.mli b/tactics/equality.mli index 304aa43ae..2cf4b3027 100644 --- a/tactics/equality.mli +++ b/tactics/equality.mli @@ -21,7 +21,7 @@ open Tacticals open Tactics open Tacexpr open Termops -open Rawterm +open Glob_term open Genarg open Ind_tables (*i*) diff --git a/tactics/evar_tactics.mli b/tactics/evar_tactics.mli index 40b628315..044ec3d3b 100644 --- a/tactics/evar_tactics.mli +++ b/tactics/evar_tactics.mli @@ -11,7 +11,7 @@ open Names open Tacexpr open Termops -val instantiate : int -> Tacinterp.interp_sign * Rawterm.glob_constr -> +val instantiate : int -> Tacinterp.interp_sign * Glob_term.glob_constr -> (identifier * hyp_location_flag, unit) location -> tactic (*i diff --git a/tactics/extraargs.ml4 b/tactics/extraargs.ml4 index e31428f7c..6bdbdb80b 100644 --- a/tactics/extraargs.ml4 +++ b/tactics/extraargs.ml4 @@ -52,7 +52,7 @@ END let pr_int_list = pr_int_list_full () () () -open Rawterm +open Glob_term let pr_occurrences _prc _prlc _prt l = match l with diff --git a/tactics/extraargs.mli b/tactics/extraargs.mli index 66c251971..5f3a8e260 100644 --- a/tactics/extraargs.mli +++ b/tactics/extraargs.mli @@ -12,7 +12,7 @@ open Names open Proof_type open Topconstr open Termops -open Rawterm +open Glob_term val rawwit_orient : bool raw_abstract_argument_type val wit_orient : bool typed_abstract_argument_type @@ -22,12 +22,12 @@ val pr_orient : bool -> Pp.std_ppcmds val occurrences : (int list or_var) Pcoq.Gram.entry val rawwit_occurrences : (int list or_var) raw_abstract_argument_type val wit_occurrences : (int list) typed_abstract_argument_type -val pr_occurrences : int list Rawterm.or_var -> Pp.std_ppcmds +val pr_occurrences : int list Glob_term.or_var -> Pp.std_ppcmds val rawwit_raw : constr_expr raw_abstract_argument_type val wit_raw : (Tacinterp.interp_sign * glob_constr) typed_abstract_argument_type val raw : constr_expr Pcoq.Gram.entry -val pr_raw : (Tacinterp.interp_sign * Rawterm.glob_constr) -> Pp.std_ppcmds +val pr_raw : (Tacinterp.interp_sign * Glob_term.glob_constr) -> Pp.std_ppcmds type 'id gen_place= ('id * hyp_location_flag,unit) location diff --git a/tactics/extratactics.ml4 b/tactics/extratactics.ml4 index 9a9ef164e..6377eafd9 100644 --- a/tactics/extratactics.ml4 +++ b/tactics/extratactics.ml4 @@ -15,7 +15,7 @@ open Extraargs open Mod_subst open Names open Tacexpr -open Rawterm +open Glob_term open Tactics open Util open Evd @@ -324,11 +324,11 @@ VERNAC COMMAND EXTEND DeriveInversionClear -> [ add_inversion_lemma_exn na c s false inv_clear_tac ] | [ "Derive" "Inversion_clear" ident(na) "with" constr(c) ] - -> [ add_inversion_lemma_exn na c (Rawterm.RProp Term.Null) false inv_clear_tac ] + -> [ add_inversion_lemma_exn na c (Glob_term.RProp Term.Null) false inv_clear_tac ] END open Term -open Rawterm +open Glob_term VERNAC COMMAND EXTEND DeriveInversion | [ "Derive" "Inversion" ident(na) "with" constr(c) "Sort" sort(s) ] @@ -395,7 +395,7 @@ END open Tactics open Tactics open Libnames -open Rawterm +open Glob_term open Summary open Libobject open Lib diff --git a/tactics/hiddentac.ml b/tactics/hiddentac.ml index 1c6d72e9e..a92330f17 100644 --- a/tactics/hiddentac.ml +++ b/tactics/hiddentac.ml @@ -10,7 +10,7 @@ open Term open Proof_type open Tacmach -open Rawterm +open Glob_term open Refiner open Genarg open Tacexpr diff --git a/tactics/hiddentac.mli b/tactics/hiddentac.mli index dd2b0bf50..8c0092980 100644 --- a/tactics/hiddentac.mli +++ b/tactics/hiddentac.mli @@ -13,7 +13,7 @@ open Proof_type open Tacmach open Genarg open Tacexpr -open Rawterm +open Glob_term open Evd open Clenv open Termops diff --git a/tactics/inv.ml b/tactics/inv.ml index 1d1ab3f9e..2ae4e22e5 100644 --- a/tactics/inv.ml +++ b/tactics/inv.ml @@ -32,7 +32,7 @@ open Equality open Typing open Pattern open Matching -open Rawterm +open Glob_term open Genarg open Tacexpr diff --git a/tactics/inv.mli b/tactics/inv.mli index e4daa082f..ef828d882 100644 --- a/tactics/inv.mli +++ b/tactics/inv.mli @@ -12,7 +12,7 @@ open Term open Tacmach open Genarg open Tacexpr -open Rawterm +open Glob_term type inversion_status = Dep of constr option | NoDep diff --git a/tactics/leminv.mli b/tactics/leminv.mli index b4b5737b5..1ac9b4d6f 100644 --- a/tactics/leminv.mli +++ b/tactics/leminv.mli @@ -1,7 +1,7 @@ open Util open Names open Term -open Rawterm +open Glob_term open Proof_type open Topconstr diff --git a/tactics/rewrite.ml4 b/tactics/rewrite.ml4 index 1faf9489b..188bc3dc5 100644 --- a/tactics/rewrite.ml4 +++ b/tactics/rewrite.ml4 @@ -26,7 +26,7 @@ open Tactics open Pattern open Clenv open Auto -open Rawterm +open Glob_term open Hiddentac open Typeclasses open Typeclasses_errors @@ -1582,7 +1582,7 @@ let setoid_transitivity c gl = let proof = get_transitive_proof env evm car rel in match c with | None -> eapply proof - | Some c -> apply_with_bindings (proof,Rawterm.ImplicitBindings [ c ])) + | Some c -> apply_with_bindings (proof,Glob_term.ImplicitBindings [ c ])) (transitivity_red true c) let setoid_symmetry_in id gl = diff --git a/tactics/tacinterp.ml b/tactics/tacinterp.ml index f193c537a..917a98c55 100644 --- a/tactics/tacinterp.ml +++ b/tactics/tacinterp.ml @@ -15,7 +15,7 @@ open Libobject open Pattern open Matching open Pp -open Rawterm +open Glob_term open Sign open Tacred open Util diff --git a/tactics/tacinterp.mli b/tactics/tacinterp.mli index ca5acad31..9d782bd41 100644 --- a/tactics/tacinterp.mli +++ b/tactics/tacinterp.mli @@ -99,8 +99,8 @@ val intern_constr : glob_sign -> constr_expr -> glob_constr_and_expr val intern_constr_with_bindings : - glob_sign -> constr_expr * constr_expr Rawterm.bindings -> - glob_constr_and_expr * glob_constr_and_expr Rawterm.bindings + glob_sign -> constr_expr * constr_expr Glob_term.bindings -> + glob_constr_and_expr * glob_constr_and_expr Glob_term.bindings val intern_hyp : glob_sign -> identifier Util.located -> identifier Util.located @@ -127,7 +127,7 @@ val interp_tac_gen : (identifier * value) list -> identifier list -> val interp_hyp : interp_sign -> goal sigma -> identifier located -> identifier -val interp_bindings : interp_sign -> Environ.env -> Evd.evar_map -> glob_constr_and_expr Rawterm.bindings -> Evd.evar_map * constr Rawterm.bindings +val interp_bindings : interp_sign -> Environ.env -> Evd.evar_map -> glob_constr_and_expr Glob_term.bindings -> Evd.evar_map * constr Glob_term.bindings (** Initial call for interpretation *) val glob_tactic : raw_tactic_expr -> glob_tactic_expr diff --git a/tactics/tacticals.ml b/tactics/tacticals.ml index dc013fda6..2598cab5e 100644 --- a/tactics/tacticals.ml +++ b/tactics/tacticals.ml @@ -21,7 +21,7 @@ open Refiner open Tacmach open Clenv open Clenvtac -open Rawterm +open Glob_term open Pattern open Matching open Genarg diff --git a/tactics/tacticals.mli b/tactics/tacticals.mli index b030a09c3..db9ab0c9b 100644 --- a/tactics/tacticals.mli +++ b/tactics/tacticals.mli @@ -19,7 +19,7 @@ open Pattern open Genarg open Tacexpr open Termops -open Rawterm +open Glob_term (** Tacticals i.e. functions from tactics to tactics. *) diff --git a/tactics/tactics.ml b/tactics/tactics.ml index 2c4201f99..11bb6b436 100644 --- a/tactics/tactics.ml +++ b/tactics/tactics.ml @@ -24,7 +24,7 @@ open Libnames open Evd open Pfedit open Tacred -open Rawterm +open Glob_term open Tacmach open Proof_type open Logic diff --git a/tactics/tactics.mli b/tactics/tactics.mli index 136815368..a2dd6e411 100644 --- a/tactics/tactics.mli +++ b/tactics/tactics.mli @@ -23,7 +23,7 @@ open Libnames open Genarg open Tacexpr open Nametab -open Rawterm +open Glob_term open Pattern open Termops diff --git a/tactics/termdn.ml b/tactics/termdn.ml index 43b94f09a..443acc6f5 100644 --- a/tactics/termdn.ml +++ b/tactics/termdn.ml @@ -11,7 +11,7 @@ open Names open Nameops open Term open Pattern -open Rawterm +open Glob_term open Libnames open Nametab diff --git a/toplevel/auto_ind_decl.ml b/toplevel/auto_ind_decl.ml index bb4d7423f..77eeac64b 100644 --- a/toplevel/auto_ind_decl.ml +++ b/toplevel/auto_ind_decl.ml @@ -512,13 +512,13 @@ let compute_bl_tact bl_scheme_key ind lnamesparrec nparrec gsig = tclTHENSEQ [ intros_using fresh_first_intros; intro_using freshn ; new_induct false [ (Tacexpr.ElimOnConstr ((mkVar freshn), - Rawterm.NoBindings))] + Glob_term.NoBindings))] None (None,None) None; intro_using freshm; new_destruct false [ (Tacexpr.ElimOnConstr ((mkVar freshm), - Rawterm.NoBindings))] + Glob_term.NoBindings))] None (None,None) None; @@ -539,7 +539,7 @@ repeat ( apply andb_prop in z;let z1:= fresh "Z" in destruct z as [z1 z]). in avoid := fresht::(!avoid); (new_destruct false [Tacexpr.ElimOnConstr - ((mkVar freshz,Rawterm.NoBindings))] + ((mkVar freshz,Glob_term.NoBindings))] None (None, Some (dl,Genarg.IntroOrAndPattern [[ dl,Genarg.IntroIdentifier fresht; @@ -650,13 +650,13 @@ let compute_lb_tact lb_scheme_key ind lnamesparrec nparrec gsig = tclTHENSEQ [ intros_using fresh_first_intros; intro_using freshn ; new_induct false [Tacexpr.ElimOnConstr - ((mkVar freshn),Rawterm.NoBindings)] + ((mkVar freshn),Glob_term.NoBindings)] None (None,None) None; intro_using freshm; new_destruct false [Tacexpr.ElimOnConstr - ((mkVar freshm),Rawterm.NoBindings)] + ((mkVar freshm),Glob_term.NoBindings)] None (None,None) None; @@ -665,7 +665,7 @@ let compute_lb_tact lb_scheme_key ind lnamesparrec nparrec gsig = tclTRY ( tclORELSE reflexivity (Equality.discr_tac false None) ); - Equality.inj [] false (mkVar freshz,Rawterm.NoBindings); + Equality.inj [] false (mkVar freshz,Glob_term.NoBindings); intros; simpl_in_concl; Auto.default_auto; tclREPEAT ( @@ -810,7 +810,7 @@ let compute_dec_tact ind lnamesparrec nparrec gsig = ) (tclTHEN (new_destruct false [Tacexpr.ElimOnConstr - (eqbnm,Rawterm.NoBindings)] + (eqbnm,Glob_term.NoBindings)] None (None,None) None) @@ -820,7 +820,7 @@ let compute_dec_tact ind lnamesparrec nparrec gsig = avoid := freshH2::(!avoid); tclTHENS ( new_destruct false [Tacexpr.ElimOnConstr - ((mkVar freshH),Rawterm.NoBindings)] + ((mkVar freshH),Glob_term.NoBindings)] None (None,Some (dl,Genarg.IntroOrAndPattern [ [dl,Genarg.IntroAnonymous]; @@ -851,7 +851,7 @@ let compute_dec_tact ind lnamesparrec nparrec gsig = all_occurrences false (List.hd !avoid) ((mkVar (List.hd (List.tl !avoid))), - Rawterm.NoBindings + Glob_term.NoBindings ) true; Equality.discr_tac false None diff --git a/toplevel/classes.ml b/toplevel/classes.ml index bf029f419..f5a450a5c 100644 --- a/toplevel/classes.ml +++ b/toplevel/classes.ml @@ -21,7 +21,7 @@ open Typeclasses_errors open Typeclasses open Libnames open Constrintern -open Rawterm +open Glob_term open Topconstr (*i*) diff --git a/toplevel/command.ml b/toplevel/command.ml index 2e6fd8f49..b37a27faf 100644 --- a/toplevel/command.ml +++ b/toplevel/command.ml @@ -319,7 +319,7 @@ let extract_params indl = let extract_inductive indl = List.map (fun ((_,indname),_,ar,lc) -> { ind_name = indname; - ind_arity = Option.cata (fun x -> x) (CSort (dummy_loc, Rawterm.RType None)) ar; + ind_arity = Option.cata (fun x -> x) (CSort (dummy_loc, Glob_term.RType None)) ar; ind_lc = List.map (fun (_,((_,id),t)) -> (id,t)) lc }) indl diff --git a/toplevel/himsg.ml b/toplevel/himsg.ml index 04e0b352c..1c677de95 100644 --- a/toplevel/himsg.ml +++ b/toplevel/himsg.ml @@ -26,7 +26,7 @@ open Reduction open Cases open Logic open Printer -open Rawterm +open Glob_term open Evd let pr_lconstr c = quote (pr_lconstr c) diff --git a/toplevel/indschemes.mli b/toplevel/indschemes.mli index a1464b80c..b26c3b88d 100644 --- a/toplevel/indschemes.mli +++ b/toplevel/indschemes.mli @@ -11,7 +11,7 @@ open Names open Term open Environ open Libnames -open Rawterm +open Glob_term open Genarg open Vernacexpr open Ind_tables diff --git a/toplevel/metasyntax.ml b/toplevel/metasyntax.ml index 7564ee8ea..e3aaaa5e9 100644 --- a/toplevel/metasyntax.ml +++ b/toplevel/metasyntax.ml @@ -19,7 +19,7 @@ open Summary open Constrintern open Vernacexpr open Pcoq -open Rawterm +open Glob_term open Libnames open Tok open Lexer diff --git a/toplevel/search.ml b/toplevel/search.ml index b2e33d1d3..d07743380 100644 --- a/toplevel/search.ml +++ b/toplevel/search.ml @@ -11,7 +11,7 @@ open Util open Names open Nameops open Term -open Rawterm +open Glob_term open Declarations open Libobject open Declare diff --git a/toplevel/vernacexpr.ml b/toplevel/vernacexpr.ml index 797fc79c6..1b8271c89 100644 --- a/toplevel/vernacexpr.ml +++ b/toplevel/vernacexpr.ml @@ -134,7 +134,7 @@ type option_ref_value = | StringRefValue of string | QualidRefValue of reference -type sort_expr = Rawterm.rawsort +type sort_expr = Glob_term.rawsort type definition_expr = | ProveBody of local_binder list * constr_expr diff --git a/toplevel/whelp.ml4 b/toplevel/whelp.ml4 index dd947fcda..a6ef73617 100644 --- a/toplevel/whelp.ml4 +++ b/toplevel/whelp.ml4 @@ -15,7 +15,7 @@ open System open Names open Term open Environ -open Rawterm +open Glob_term open Libnames open Nametab open Detyping |