diff options
Diffstat (limited to 'toplevel')
| -rw-r--r-- | toplevel/auto_ind_decl.ml | 18 | ||||
| -rw-r--r-- | toplevel/classes.ml | 2 | ||||
| -rw-r--r-- | toplevel/command.ml | 2 | ||||
| -rw-r--r-- | toplevel/himsg.ml | 2 | ||||
| -rw-r--r-- | toplevel/indschemes.mli | 2 | ||||
| -rw-r--r-- | toplevel/metasyntax.ml | 2 | ||||
| -rw-r--r-- | toplevel/search.ml | 2 | ||||
| -rw-r--r-- | toplevel/vernacexpr.ml | 2 | ||||
| -rw-r--r-- | toplevel/whelp.ml4 | 2 |
9 files changed, 17 insertions, 17 deletions
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 |