diff options
Diffstat (limited to 'toplevel')
| -rw-r--r-- | toplevel/command.ml | 2 | ||||
| -rw-r--r-- | toplevel/indschemes.mli | 2 | ||||
| -rw-r--r-- | toplevel/record.ml | 2 | ||||
| -rw-r--r-- | toplevel/vernacexpr.ml | 2 | ||||
| -rw-r--r-- | toplevel/whelp.ml4 | 10 |
5 files changed, 9 insertions, 9 deletions
diff --git a/toplevel/command.ml b/toplevel/command.ml index b37a27faf..93b05290f 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, Glob_term.RType None)) ar; + ind_arity = Option.cata (fun x -> x) (CSort (dummy_loc, Glob_term.GType None)) ar; ind_lc = List.map (fun (_,((_,id),t)) -> (id,t)) lc }) indl diff --git a/toplevel/indschemes.mli b/toplevel/indschemes.mli index b26c3b88d..87aedc7be 100644 --- a/toplevel/indschemes.mli +++ b/toplevel/indschemes.mli @@ -35,7 +35,7 @@ val declare_rewriting_schemes : inductive -> unit (** Mutual Minimality/Induction scheme *) val do_mutual_induction_scheme : - (identifier located * bool * inductive * rawsort) list -> unit + (identifier located * bool * inductive * glob_sort) list -> unit (** Main calls to interpret the Scheme command *) diff --git a/toplevel/record.ml b/toplevel/record.ml index 707e0dc4a..ea11ca487 100644 --- a/toplevel/record.ml +++ b/toplevel/record.ml @@ -30,7 +30,7 @@ open Topconstr let interp_evars evdref env impls k typ = let typ' = intern_gen true ~impls !evdref env typ in - let imps = Implicit_quantifiers.implicits_of_rawterm typ' in + let imps = Implicit_quantifiers.implicits_of_glob_constr typ' in imps, Pretyping.Default.understand_tcc_evars evdref env k typ' let interp_fields_evars evars env nots l = diff --git a/toplevel/vernacexpr.ml b/toplevel/vernacexpr.ml index 1b8271c89..9af222461 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 = Glob_term.rawsort +type sort_expr = Glob_term.glob_sort type definition_expr = | ProveBody of local_binder list * constr_expr diff --git a/toplevel/whelp.ml4 b/toplevel/whelp.ml4 index a6ef73617..67f54b523 100644 --- a/toplevel/whelp.ml4 +++ b/toplevel/whelp.ml4 @@ -91,10 +91,10 @@ let uri_of_repr_kn ref (mp,dir,l) = let url_paren f l = url_char '('; f l; url_char ')' let url_bracket f l = url_char '['; f l; url_char ']' -let whelp_of_rawsort = function - | RProp Null -> "Prop" - | RProp Pos -> "Set" - | RType _ -> "Type" +let whelp_of_glob_sort = function + | GProp Null -> "Prop" + | GProp Pos -> "Set" + | GType _ -> "Type" let uri_int n = Buffer.add_string b (string_of_int n) @@ -144,7 +144,7 @@ let rec uri_of_constr c = | GVar (_,id) -> url_id id | GRef (_,ref) -> uri_of_global ref | GHole _ | GEvar _ -> url_string "?" - | GSort (_,s) -> url_string (whelp_of_rawsort s) + | GSort (_,s) -> url_string (whelp_of_glob_sort s) | _ -> url_paren (fun () -> match c with | GApp (_,f,args) -> let inst,rest = merge (section_parameters f) args in |