diff options
51 files changed, 200 insertions, 200 deletions
diff --git a/interp/constrextern.ml b/interp/constrextern.ml index 9215f9b51..fa0e18915 100644 --- a/interp/constrextern.ml +++ b/interp/constrextern.ml @@ -487,7 +487,7 @@ let rec flatten_application = function | a -> a (**********************************************************************) -(* mapping rawterms to numerals (in presence of coercions, choose the *) +(* mapping glob_constr to numerals (in presence of coercions, choose the *) (* one with no delimiter if possible) *) let extern_possible_prim_token scopes r = @@ -507,12 +507,12 @@ let extern_optimal_prim_token scopes r r' = | _ -> raise No_match (**********************************************************************) -(* mapping rawterms to constr_expr *) +(* mapping glob_constr to constr_expr *) -let extern_rawsort = function - | RProp _ as s -> s - | RType (Some _) as s when !print_universes -> s - | RType _ -> RType None +let extern_glob_sort = function + | GProp _ as s -> s + | GType (Some _) as s when !print_universes -> s + | GType _ -> GType None let rec extern inctx scopes vars r = let r' = remove_coercions inctx r in @@ -646,7 +646,7 @@ let rec extern inctx scopes vars r = | GRec (loc,fk,idv,blv,tyv,bv) -> let vars' = Array.fold_right Idset.add idv vars in (match fk with - | RFix (nv,n) -> + | GFix (nv,n) -> let listdecl = Array.mapi (fun i fi -> let (bl,ty,def) = blv.(i), tyv.(i), bv.(i) in @@ -663,7 +663,7 @@ let rec extern inctx scopes vars r = extern false scopes vars1 def)) idv in CFix (loc,(loc,idv.(n)),Array.to_list listdecl) - | RCoFix n -> + | GCoFix n -> let listdecl = Array.mapi (fun i fi -> let (ids,bl) = extern_local_binder scopes vars blv.(i) in @@ -674,7 +674,7 @@ let rec extern inctx scopes vars r = in CCoFix (loc,(loc,idv.(n)),Array.to_list listdecl)) - | GSort (loc,s) -> CSort (loc,extern_rawsort s) + | GSort (loc,s) -> CSort (loc,extern_glob_sort s) | GHole (loc,e) -> CHole (loc, Some e) @@ -809,9 +809,9 @@ and extern_symbol (tmp_scope,scopes as allscopes) vars t = function No_match -> extern_symbol allscopes vars t rules and extern_recursion_order scopes vars = function - RStructRec -> CStructRec - | RWfRec c -> CWfRec (extern true scopes vars c) - | RMeasureRec (m,r) -> CMeasureRec (extern true scopes vars m, + GStructRec -> CStructRec + | GWfRec c -> CWfRec (extern true scopes vars c) + | GMeasureRec (m,r) -> CMeasureRec (extern true scopes vars m, Option.map (extern true scopes vars) r) @@ -843,15 +843,15 @@ let extern_type at_top env t = let r = Detyping.detype at_top avoid (names_of_rel_context env) t in extern_glob_type (vars_of_env env) r -let extern_sort s = extern_rawsort (detype_sort s) +let extern_sort s = extern_glob_sort (detype_sort s) (******************************************************************) (* Main translation function from pattern -> constr_expr *) -let rec raw_of_pat env = function +let rec glob_of_pat env = function | PRef ref -> GRef (loc,ref) | PVar id -> GVar (loc,id) - | PEvar (n,l) -> GEvar (loc,n,Some (array_map_to_list (raw_of_pat env) l)) + | PEvar (n,l) -> GEvar (loc,n,Some (array_map_to_list (glob_of_pat env) l)) | PRel n -> let id = try match lookup_name_of_rel n env with | Name id -> id @@ -862,26 +862,26 @@ let rec raw_of_pat env = function | PMeta None -> GHole (loc,Evd.InternalHole) | PMeta (Some n) -> GPatVar (loc,(false,n)) | PApp (f,args) -> - GApp (loc,raw_of_pat env f,array_map_to_list (raw_of_pat env) args) + GApp (loc,glob_of_pat env f,array_map_to_list (glob_of_pat env) args) | PSoApp (n,args) -> GApp (loc,GPatVar (loc,(true,n)), - List.map (raw_of_pat env) args) + List.map (glob_of_pat env) args) | PProd (na,t,c) -> - GProd (loc,na,Explicit,raw_of_pat env t,raw_of_pat (na::env) c) + GProd (loc,na,Explicit,glob_of_pat env t,glob_of_pat (na::env) c) | PLetIn (na,t,c) -> - GLetIn (loc,na,raw_of_pat env t, raw_of_pat (na::env) c) + GLetIn (loc,na,glob_of_pat env t, glob_of_pat (na::env) c) | PLambda (na,t,c) -> - GLambda (loc,na,Explicit,raw_of_pat env t, raw_of_pat (na::env) c) + GLambda (loc,na,Explicit,glob_of_pat env t, glob_of_pat (na::env) c) | PIf (c,b1,b2) -> - GIf (loc, raw_of_pat env c, (Anonymous,None), - raw_of_pat env b1, raw_of_pat env b2) + GIf (loc, glob_of_pat env c, (Anonymous,None), + glob_of_pat env b1, glob_of_pat env b2) | PCase ((LetStyle,[|n|],ind,None),PMeta None,tm,[|b|]) -> - let nal,b = it_destRLambda_or_LetIn_names n (raw_of_pat env b) in - GLetTuple (loc,nal,(Anonymous,None),raw_of_pat env tm,b) + let nal,b = it_destRLambda_or_LetIn_names n (glob_of_pat env b) in + GLetTuple (loc,nal,(Anonymous,None),glob_of_pat env tm,b) | PCase (_,PMeta None,tm,[||]) -> - GCases (loc,RegularStyle,None,[raw_of_pat env tm,(Anonymous,None)],[]) + GCases (loc,RegularStyle,None,[glob_of_pat env tm,(Anonymous,None)],[]) | PCase ((_,cstr_nargs,indo,ind_nargs),p,tm,bv) -> - let brs = Array.to_list (Array.map (raw_of_pat env) bv) in + let brs = Array.to_list (Array.map (glob_of_pat env) bv) in let brns = Array.to_list cstr_nargs in (* ind is None only if no branch and no return type *) let ind = Option.get indo in @@ -890,14 +890,14 @@ let rec raw_of_pat env = function if p = PMeta None then (Anonymous,None),None else let nparams,n = Option.get ind_nargs in - return_type_of_predicate ind nparams n (raw_of_pat env p) in - GCases (loc,RegularStyle,rtn,[raw_of_pat env tm,indnames],mat) + return_type_of_predicate ind nparams n (glob_of_pat env p) in + GCases (loc,RegularStyle,rtn,[glob_of_pat env tm,indnames],mat) | PFix f -> Detyping.detype false [] env (mkFix f) | PCoFix c -> Detyping.detype false [] env (mkCoFix c) | PSort s -> GSort (loc,s) let extern_constr_pattern env pat = - extern true (None,[]) Idset.empty (raw_of_pat env pat) + extern true (None,[]) Idset.empty (glob_of_pat env pat) let extern_rel_context where env sign = let a = detype_rel_context where [] (names_of_rel_context env) sign in diff --git a/interp/constrextern.mli b/interp/constrextern.mli index 033090fc9..e1fdd068b 100644 --- a/interp/constrextern.mli +++ b/interp/constrextern.mli @@ -21,7 +21,7 @@ open Notation val check_same_type : constr_expr -> constr_expr -> unit -(** Translation of pattern, cases pattern, rawterm and term into syntax +(** Translation of pattern, cases pattern, glob_constr and term into syntax trees for printing *) val extern_cases_pattern : Idset.t -> cases_pattern -> cases_pattern_expr @@ -36,7 +36,7 @@ val extern_constr : bool -> env -> constr -> constr_expr val extern_constr_in_scope : bool -> scope_name -> env -> constr -> constr_expr val extern_reference : loc -> Idset.t -> global_reference -> reference val extern_type : bool -> env -> types -> constr_expr -val extern_sort : sorts -> rawsort +val extern_sort : sorts -> glob_sort val extern_rel_context : constr option -> env -> rel_context -> local_binder list diff --git a/interp/constrintern.ml b/interp/constrintern.ml index 4e8d0a621..1b3cedd77 100644 --- a/interp/constrintern.ml +++ b/interp/constrintern.ml @@ -1134,17 +1134,17 @@ let internalize sigma globalenv env allow_patvar lvar c = let n, ro, ((ids',_,_,_),rbl) = match order with | CStructRec -> - intern_ro_arg (fun _ -> RStructRec) + intern_ro_arg (fun _ -> GStructRec) | CWfRec c -> - intern_ro_arg (fun f -> RWfRec (f c)) + intern_ro_arg (fun f -> GWfRec (f c)) | CMeasureRec (m,r) -> - intern_ro_arg (fun f -> RMeasureRec (f m, Option.map f r)) + intern_ro_arg (fun f -> GMeasureRec (f m, Option.map f r)) in let ids'' = List.fold_right Idset.add lf ids' in ((n, ro), List.rev rbl, intern_type (ids',unb,tmp_scope,scopes) ty, intern (ids'',unb,None,scopes) bd)) dl in - GRec (loc,RFix + GRec (loc,GFix (Array.map (fun (ro,_,_,_) -> ro) idl,n), Array.of_list lf, Array.map (fun (_,bl,_,_) -> bl) idl, @@ -1166,7 +1166,7 @@ let internalize sigma globalenv env allow_patvar lvar c = (List.rev rbl, intern_type (ids',unb,tmp_scope,scopes) ty, intern (ids'',unb,None,scopes) bd)) dl in - GRec (loc,RCoFix n, + GRec (loc,GCoFix n, Array.of_list lf, Array.map (fun (bl,_,_) -> bl) idl, Array.map (fun (_,ty,_) -> ty) idl, @@ -1504,7 +1504,7 @@ let interp_constr_evars_gen_impls ?evdref ?(fail_evar=true) in let istype = kind = IsType in let c = intern_gen istype ~impls !evdref env c in - let imps = Implicit_quantifiers.implicits_of_rawterm ~with_products:istype c in + let imps = Implicit_quantifiers.implicits_of_glob_constr ~with_products:istype c in Default.understand_tcc_evars ~fail_evar evdref env kind c, imps let interp_casted_constr_evars_impls ?evdref ?(fail_evar=true) diff --git a/interp/genarg.mli b/interp/genarg.mli index 08839698a..54aadba18 100644 --- a/interp/genarg.mli +++ b/interp/genarg.mli @@ -171,8 +171,8 @@ val rawwit_quant_hyp : (quantified_hypothesis,rlevel) abstract_argument_type val globwit_quant_hyp : (quantified_hypothesis,glevel) abstract_argument_type val wit_quant_hyp : (quantified_hypothesis,tlevel) abstract_argument_type -val rawwit_sort : (rawsort,rlevel) abstract_argument_type -val globwit_sort : (rawsort,glevel) abstract_argument_type +val rawwit_sort : (glob_sort,rlevel) abstract_argument_type +val globwit_sort : (glob_sort,glevel) abstract_argument_type val wit_sort : (sorts,tlevel) abstract_argument_type val rawwit_constr : (constr_expr,rlevel) abstract_argument_type diff --git a/interp/implicit_quantifiers.ml b/interp/implicit_quantifiers.ml index b430c000b..428ddd6ab 100644 --- a/interp/implicit_quantifiers.ml +++ b/interp/implicit_quantifiers.ml @@ -293,7 +293,7 @@ let implicit_application env ?(allow_partial=true) f ty = CAppExpl (loc, (None, id), args), avoid in c, avoid -let implicits_of_rawterm ?(with_products=true) l = +let implicits_of_glob_constr ?(with_products=true) l = let rec aux i c = let abs loc na bk t b = let rest = aux (succ i) b in diff --git a/interp/implicit_quantifiers.mli b/interp/implicit_quantifiers.mli index cb782e0c5..05f54ec75 100644 --- a/interp/implicit_quantifiers.mli +++ b/interp/implicit_quantifiers.mli @@ -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 -> Glob_term.glob_constr -> (Topconstr.explicitation * (bool * bool * bool)) list +val implicits_of_glob_constr : ?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 37c9ddbeb..86a515537 100644 --- a/interp/notation.ml +++ b/interp/notation.ml @@ -176,7 +176,7 @@ type interp_rule = | NotationRule of scope_name option * notation | SynDefRule of kernel_name -(* We define keys for rawterm and aconstr to split the syntax entries +(* We define keys for glob_constr and aconstr to split the syntax entries according to the key of the pattern (adapted from Chet Murthy by HH) *) type key = diff --git a/interp/topconstr.ml b/interp/topconstr.ml index 0e0326808..f8c0aeb87 100644 --- a/interp/topconstr.ml +++ b/interp/topconstr.ml @@ -44,7 +44,7 @@ type aconstr = | ARec of fix_kind * identifier array * (name * aconstr option * aconstr) list array * aconstr array * aconstr array - | ASort of rawsort + | ASort of glob_sort | AHole of Evd.hole_kind | APatVar of patvar | ACast of aconstr * aconstr cast_type @@ -552,8 +552,8 @@ let bind_binder (sigma,sigmalist,sigmabinders) x bl = let match_fix_kind fk1 fk2 = match (fk1,fk2) with - | RCoFix n1, RCoFix n2 -> n1 = n2 - | RFix (nl1,n1), RFix (nl2,n2) -> + | GCoFix n1, GCoFix n2 -> n1 = n2 + | GFix (nl1,n1), GFix (nl2,n2) -> n1 = n2 && array_for_all2 (fun (n1,_) (n2,_) -> n2 = None || n1 = n2) nl1 nl2 | _ -> false @@ -843,7 +843,7 @@ type constr_expr = | CHole of loc * Evd.hole_kind option | CPatVar of loc * (bool * patvar) | CEvar of loc * existential_key * constr_expr list option - | CSort of loc * rawsort + | CSort of loc * glob_sort | CCast of loc * constr_expr * constr_expr cast_type | CNotation of loc * notation * constr_notation_substitution | CGeneralization of loc * binding_kind * abstraction_kind option * constr_expr diff --git a/interp/topconstr.mli b/interp/topconstr.mli index b01c35093..405db2d17 100644 --- a/interp/topconstr.mli +++ b/interp/topconstr.mli @@ -41,7 +41,7 @@ type aconstr = | ARec of fix_kind * identifier array * (name * aconstr option * aconstr) list array * aconstr array * aconstr array - | ASort of rawsort + | ASort of glob_sort | AHole of Evd.hole_kind | APatVar of patvar | ACast of aconstr * aconstr cast_type @@ -158,7 +158,7 @@ type constr_expr = | CHole of loc * Evd.hole_kind option | CPatVar of loc * (bool * patvar) | CEvar of loc * existential_key * constr_expr list option - | CSort of loc * rawsort + | CSort of loc * glob_sort | CCast of loc * constr_expr * constr_expr cast_type | CNotation of loc * notation * constr_notation_substitution | CGeneralization of loc * binding_kind * abstraction_kind option * constr_expr diff --git a/parsing/g_constr.ml4 b/parsing/g_constr.ml4 index d8574409d..6a01ff1dc 100644 --- a/parsing/g_constr.ml4 +++ b/parsing/g_constr.ml4 @@ -133,9 +133,9 @@ GEXTEND Gram [ [ c = lconstr -> c ] ] ; sort: - [ [ "Set" -> RProp Pos - | "Prop" -> RProp Null - | "Type" -> RType None ] ] + [ [ "Set" -> GProp Pos + | "Prop" -> GProp Null + | "Type" -> GType None ] ] ; lconstr: [ [ c = operconstr LEVEL "200" -> c ] ] diff --git a/parsing/g_xml.ml4 b/parsing/g_xml.ml4 index 18bc1ff78..72634b08e 100644 --- a/parsing/g_xml.ml4 +++ b/parsing/g_xml.ml4 @@ -95,9 +95,9 @@ let inductive_of_cdata a = match global_of_cdata a with let ltacref_of_cdata (loc,a) = (loc,locate_tactic (uri_of_data a)) let sort_of_cdata (loc,a) = match a with - | "Prop" -> RProp Null - | "Set" -> RProp Pos - | "Type" -> RType None + | "Prop" -> GProp Null + | "Set" -> GProp Pos + | "Type" -> GType None | _ -> user_err_loc (loc,"",str "sort expected.") let get_xml_sort al = sort_of_cdata (get_xml_attr "value" al) @@ -184,10 +184,10 @@ let rec interp_xml_constr = function let li,lnct = List.split (List.map interp_xml_FixFunction xl) in let ln,lc,lt = list_split3 lnct in let lctx = List.map (fun _ -> []) ln in - GRec (loc, RFix (Array.of_list li, get_xml_noFun al), Array.of_list ln, Array.of_list lctx, Array.of_list lc, Array.of_list lt) + GRec (loc, GFix (Array.of_list li, get_xml_noFun al), Array.of_list ln, Array.of_list lctx, Array.of_list lc, Array.of_list lt) | XmlTag (loc,"COFIX",al,xl) -> let ln,lc,lt = list_split3 (List.map interp_xml_CoFixFunction xl) in - GRec (loc, RCoFix (get_xml_noFun al), Array.of_list ln, [||], Array.of_list lc, Array.of_list lt) + GRec (loc, GCoFix (get_xml_noFun al), Array.of_list ln, [||], Array.of_list lc, Array.of_list lt) | XmlTag (loc,"CAST",al,[x1;x2]) -> GCast (loc, interp_xml_term x1, CastConv (DEFAULTcast, interp_xml_type x2)) | XmlTag (loc,"SORT",al,[]) -> @@ -229,15 +229,15 @@ and interp_xml_recursionOrder x = let (locs, s) = get_xml_attr "type" al in match s with "Structural" -> - (match l with [] -> RStructRec + (match l with [] -> GStructRec | _ -> error_expect_no_argument loc) | "WellFounded" -> (match l with - [c] -> RWfRec (interp_xml_type c) + [c] -> GWfRec (interp_xml_type c) | _ -> error_expect_one_argument loc) | "Measure" -> (match l with - [m;r] -> RMeasureRec (interp_xml_type m, Some (interp_xml_type r)) + [m;r] -> GMeasureRec (interp_xml_type m, Some (interp_xml_type r)) | _ -> error_expect_two_arguments loc) | _ -> user_err_loc (locs,"",str "Invalid recursion order.") @@ -249,7 +249,7 @@ and interp_xml_FixFunction x = interp_xml_recursionOrder x1), (get_xml_name al, interp_xml_type x2, interp_xml_body x3)) | (loc,al,[x1;x2]) -> - ((Some (nmtoken (get_xml_attr "recIndex" al)), RStructRec), + ((Some (nmtoken (get_xml_attr "recIndex" al)), GStructRec), (get_xml_name al, interp_xml_type x1, interp_xml_body x2)) | (loc,_,_) -> error_expect_one_argument loc diff --git a/parsing/pcoq.mli b/parsing/pcoq.mli index 68d434a2b..bba0e5602 100644 --- a/parsing/pcoq.mli +++ b/parsing/pcoq.mli @@ -187,7 +187,7 @@ module Constr : val operconstr : constr_expr Gram.entry val ident : identifier Gram.entry val global : reference Gram.entry - val sort : rawsort Gram.entry + val sort : glob_sort Gram.entry val pattern : cases_pattern_expr Gram.entry val constr_pattern : constr_expr Gram.entry val lconstr_pattern : constr_expr Gram.entry diff --git a/parsing/ppconstr.ml b/parsing/ppconstr.ml index 9e9d21a3d..54dd550d8 100644 --- a/parsing/ppconstr.ml +++ b/parsing/ppconstr.ml @@ -108,10 +108,10 @@ let pr_in_comment pr x = str "(* " ++ pr x ++ str " *)" let pr_universe = Univ.pr_uni -let pr_rawsort = function - | RProp Term.Null -> str "Prop" - | RProp Term.Pos -> str "Set" - | RType u -> hov 0 (str "Type" ++ pr_opt (pr_in_comment pr_universe) u) +let pr_glob_sort = function + | GProp Term.Null -> str "Prop" + | GProp Term.Pos -> str "Set" + | GType u -> hov 0 (str "Type" ++ pr_opt (pr_in_comment pr_universe) u) let pr_id = pr_id let pr_name = pr_name @@ -515,7 +515,7 @@ let pr pr sep inherited a = | CHole _ -> str "_", latom | CEvar (_,n,l) -> pr_evar (pr mt) n l, latom | CPatVar (_,(_,p)) -> str "?" ++ pr_patvar p, latom - | CSort (_,s) -> pr_rawsort s, latom + | CSort (_,s) -> pr_glob_sort s, latom | CCast (_,a,CastConv (k,b)) -> let s = match k with VMcast -> "<:" | DEFAULTcast -> ":" in hv 0 (pr mt (lcast,L) a ++ cut () ++ str s ++ pr mt (-lcast,E) b), diff --git a/parsing/ppconstr.mli b/parsing/ppconstr.mli index 49791d595..f9ed3af02 100644 --- a/parsing/ppconstr.mli +++ b/parsing/ppconstr.mli @@ -56,7 +56,7 @@ val pr_may_eval : ('a -> std_ppcmds) -> ('a -> std_ppcmds) -> ('b -> std_ppcmds) -> ('c -> std_ppcmds) -> ('a,'b,'c) may_eval -> std_ppcmds -val pr_rawsort : rawsort -> std_ppcmds +val pr_glob_sort : glob_sort -> std_ppcmds val pr_binders : local_binder list -> std_ppcmds val pr_constr_pattern_expr : constr_pattern_expr -> std_ppcmds @@ -84,7 +84,7 @@ val default_term_pr : term_pr for instance if we want to build a printer which prints "Prop" as "Omega" instead we can proceed as follows: let my_modular_constr_pr pr s p = function - | CSort (_,RProp Null) -> str "Omega" + | CSort (_,GProp Null) -> str "Omega" | t -> modular_constr_pr pr s p t Which has the same type. We can turn a modular printer into a printer by taking its fixpoint. *) diff --git a/parsing/pptactic.ml b/parsing/pptactic.ml index 015dc9c08..9da14d8fa 100644 --- a/parsing/pptactic.ml +++ b/parsing/pptactic.ml @@ -140,7 +140,7 @@ let rec pr_raw_generic prc prlc prtac prpat prref (x:Genarg.rlevel Genarg.generi | IdentArgType b -> if_pattern_ident b pr_id (out_gen rawwit_ident x) | VarArgType -> pr_located pr_id (out_gen rawwit_var x) | RefArgType -> prref (out_gen rawwit_ref x) - | SortArgType -> pr_rawsort (out_gen rawwit_sort x) + | SortArgType -> pr_glob_sort (out_gen rawwit_sort x) | ConstrArgType -> prc (out_gen rawwit_constr x) | ConstrMayEvalArgType -> pr_may_eval prc prlc (pr_or_by_notation prref) prpat @@ -183,7 +183,7 @@ let rec pr_glob_generic prc prlc prtac prpat x = | IdentArgType b -> if_pattern_ident b pr_id (out_gen globwit_ident x) | VarArgType -> pr_located pr_id (out_gen globwit_var x) | RefArgType -> pr_or_var (pr_located pr_global) (out_gen globwit_ref x) - | SortArgType -> pr_rawsort (out_gen globwit_sort x) + | SortArgType -> pr_glob_sort (out_gen globwit_sort x) | ConstrArgType -> prc (out_gen globwit_constr x) | ConstrMayEvalArgType -> pr_may_eval prc prlc @@ -954,7 +954,7 @@ and pr_tacarg = function in (pr_tac, pr_match_rule) -let strip_prod_binders_rawterm n (ty,_) = +let strip_prod_binders_glob_constr n (ty,_) = let rec strip_ty acc n ty = if n=0 then (List.rev acc, (ty,None)) else match ty with @@ -1008,7 +1008,7 @@ let rec glob_printers = pr_ltac_or_var (pr_located pr_ltac_constant), pr_lident, pr_glob_extend, - strip_prod_binders_rawterm) + strip_prod_binders_glob_constr) and pr_glob_tactic_level env n (t:glob_tactic_expr) = fst (make_pr_tac glob_printers env) n t diff --git a/parsing/ppvernac.ml b/parsing/ppvernac.ml index b5367048a..8d74fd1f8 100644 --- a/parsing/ppvernac.ml +++ b/parsing/ppvernac.ml @@ -307,7 +307,7 @@ let pr_onescheme (idop,schem) = ) ++ hov 0 ((if dep then str"Induction for" else str"Minimality for") ++ spc() ++ pr_smart_global ind) ++ spc() ++ - hov 0 (str"Sort" ++ spc() ++ pr_rawsort s) + hov 0 (str"Sort" ++ spc() ++ pr_glob_sort s) | CaseScheme (dep,ind,s) -> (match idop with | Some id -> hov 0 (pr_lident id ++ str" :=") ++ spc() @@ -315,7 +315,7 @@ let pr_onescheme (idop,schem) = ) ++ hov 0 ((if dep then str"Elimination for" else str"Case for") ++ spc() ++ pr_smart_global ind) ++ spc() ++ - hov 0 (str"Sort" ++ spc() ++ pr_rawsort s) + hov 0 (str"Sort" ++ spc() ++ pr_glob_sort s) | EqualityScheme ind -> (match idop with | Some id -> hov 0 (pr_lident id ++ str" :=") ++ spc() @@ -673,7 +673,7 @@ let rec pr_vernac = function (* str"Class" ++ spc () ++ pr_lident id ++ *) (* (\* prlist_with_sep (spc) (pr_lident_constr (spc() ++ str ":" ++ spc())) par ++ *\) *) (* pr_and_type_binders_arg par ++ *) -(* (match ar with Some ar -> spc () ++ str":" ++ spc() ++ pr_rawsort (snd ar) | None -> mt()) ++ *) +(* (match ar with Some ar -> spc () ++ str":" ++ spc() ++ pr_glob_sort (snd ar) | None -> mt()) ++ *) (* spc () ++ str":=" ++ spc () ++ *) (* prlist_with_sep (fun () -> str";" ++ spc()) *) (* (fun (lid,oc,c) -> pr_lident_constr ((if oc then str" :>" else str" :") ++ spc()) (lid,c)) props ) *) diff --git a/parsing/printer.ml b/parsing/printer.ml index a7fa08f50..f1f5d4c9f 100644 --- a/parsing/printer.ml +++ b/parsing/printer.ml @@ -109,7 +109,7 @@ let pr_lconstr_pattern t = let pr_constr_pattern t = pr_constr_pattern_expr (extern_constr_pattern Termops.empty_names_context t) -let pr_sort s = pr_rawsort (extern_sort s) +let pr_sort s = pr_glob_sort (extern_sort s) let _ = Termops.set_print_constr pr_lconstr_env @@ -127,7 +127,7 @@ let pr_constructor env cstr = pr_lconstr_env env (mkConstruct cstr) let pr_evaluable_reference ref = pr_global (Tacred.global_of_evaluable_reference ref) -(*let pr_rawterm t = +(*let pr_glob_constr t = pr_lconstr (Constrextern.extern_glob_constr Idset.empty t)*) (*open Pattern diff --git a/parsing/q_constr.ml4 b/parsing/q_constr.ml4 index c8451afb1..605432692 100644 --- a/parsing/q_constr.ml4 +++ b/parsing/q_constr.ml4 @@ -33,9 +33,9 @@ EXTEND <:expr< snd (Pattern.pattern_of_glob_constr $c$) >> ] ] ; sort: - [ [ "Set" -> RProp Pos - | "Prop" -> RProp Null - | "Type" -> RType None ] ] + [ [ "Set" -> GProp Pos + | "Prop" -> GProp Null + | "Type" -> GType None ] ] ; ident: [ [ s = string -> <:expr< Names.id_of_string $str:s$ >> ] ] diff --git a/plugins/decl_mode/decl_interp.ml b/plugins/decl_mode/decl_interp.ml index 3a3f50ac8..a75f0e20b 100644 --- a/plugins/decl_mode/decl_interp.ml +++ b/plugins/decl_mode/decl_interp.ml @@ -193,7 +193,7 @@ let abstract_one_hyp inject h raw = let glob_constr_of_hyps inject hyps head = List.fold_right (abstract_one_hyp inject) hyps head -let raw_prop = GSort (dummy_loc,RProp Null) +let glob_prop = GSort (dummy_loc,GProp Null) let rec match_hyps blend names constr = function [] -> [],substl names constr @@ -214,7 +214,7 @@ let interp_hyps_gen inject blend sigma env hyps head = let constr=understand sigma env (glob_constr_of_hyps inject hyps head) in match_hyps blend [] constr hyps -let interp_hyps sigma env hyps = fst (interp_hyps_gen fst (fun x _ -> x) sigma env hyps raw_prop) +let interp_hyps sigma env hyps = fst (interp_hyps_gen fst (fun x _ -> x) sigma env hyps glob_prop) let dummy_prefix= id_of_string "__" @@ -232,7 +232,7 @@ let rec deanonymize ids = | PatCstr(loc,cstr,lpat,nam) -> PatCstr(loc,cstr,List.map (deanonymize ids) lpat,nam) -let rec raw_of_pat = +let rec glob_of_pat = function PatVar (loc,Anonymous) -> anomaly "Anonymous pattern variable" | PatVar (loc,Name id) -> @@ -243,7 +243,7 @@ let rec raw_of_pat = if n<=0 then q else add_params (pred n) (GHole(dummy_loc, Evd.TomatchTypeParameter(ind,n))::q) in - let args = List.map raw_of_pat lpat in + let args = List.map glob_of_pat lpat in raw_app(loc,GRef(dummy_loc,Libnames.ConstructRef cstr), add_params mind.Declarations.mind_nparams args) @@ -261,7 +261,7 @@ let prod_one_id (loc,id) raw = GHole (loc,Evd.BinderType (Name id)), raw) let let_in_one_alias (id,pat) raw = - GLetIn (dummy_loc,Name id, raw_of_pat pat, raw) + GLetIn (dummy_loc,Name id, glob_of_pat pat, raw) let rec bind_primary_aliases map pat = match pat with @@ -343,22 +343,22 @@ 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) -> Glob_term.GSort(dummy_loc,RProp Null) + Thesis (Plain) -> Glob_term.GSort(dummy_loc,GProp 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."); - Glob_term.GSort(dummy_loc,RProp Null) + Glob_term.GSort(dummy_loc,GProp Null) | This (c,_) -> c in - let term1 = glob_constr_of_hyps inject hyps raw_prop in + let term1 = glob_constr_of_hyps inject hyps glob_prop in let loc_ids,npatt = let rids=ref ([],pat_vars) in let npatt= deanonymize rids patt in List.rev (fst !rids),npatt in let term2 = GLetIn(dummy_loc,Anonymous, - GCast(dummy_loc,raw_of_pat npatt, + GCast(dummy_loc,glob_of_pat npatt, CastConv (DEFAULTcast,app_ind)),term1) in let term3=List.fold_right let_in_one_alias aliases term2 in let term4=List.fold_right prod_one_id loc_ids term3 in diff --git a/plugins/funind/functional_principles_types.ml b/plugins/funind/functional_principles_types.ml index c297f4965..0cc5af99f 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*Glob_term.rawsort) list) : Entries.definition_entry list = +let make_scheme (fas : (constant*Glob_term.glob_sort) 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 24c8359dc..1c02c16ec 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*Glob_term.rawsort) list -> Entries.definition_entry list +val make_scheme : (constant*Glob_term.glob_sort) list -> Entries.definition_entry list -val build_scheme : (identifier*Libnames.reference*Glob_term.rawsort) list -> unit -val build_case_scheme : (identifier*Libnames.reference*Glob_term.rawsort) -> unit +val build_scheme : (identifier*Libnames.reference*Glob_term.glob_sort) list -> unit +val build_case_scheme : (identifier*Libnames.reference*Glob_term.glob_sort) -> unit diff --git a/plugins/funind/g_indfun.ml4 b/plugins/funind/g_indfun.ml4 index 90f7b5970..fb053c032 100644 --- a/plugins/funind/g_indfun.ml4 +++ b/plugins/funind/g_indfun.ml4 @@ -167,7 +167,7 @@ END let pr_fun_scheme_arg (princ_name,fun_name,s) = Nameops.pr_id princ_name ++ str " :=" ++ spc() ++ str "Induction for " ++ Libnames.pr_reference fun_name ++ spc() ++ str "Sort " ++ - Ppconstr.pr_rawsort s + Ppconstr.pr_glob_sort s VERNAC ARGUMENT EXTEND fun_scheme_arg PRINTED BY pr_fun_scheme_arg diff --git a/plugins/funind/glob_term_to_relation.ml b/plugins/funind/glob_term_to_relation.ml index ce224d1aa..62cf3ccba 100644 --- a/plugins/funind/glob_term_to_relation.ml +++ b/plugins/funind/glob_term_to_relation.ml @@ -1200,7 +1200,7 @@ let rec rebuild_return_type rt = Topconstr.CArrow(loc,t,rebuild_return_type t') | Topconstr.CLetIn(loc,na,t,t') -> Topconstr.CLetIn(loc,na,t,rebuild_return_type t') - | _ -> Topconstr.CArrow(dummy_loc,rt,Topconstr.CSort(dummy_loc,RType None)) + | _ -> Topconstr.CArrow(dummy_loc,rt,Topconstr.CSort(dummy_loc,GType None)) let do_build_inductive diff --git a/plugins/funind/glob_termops.ml b/plugins/funind/glob_termops.ml index 0cf91f38c..3fa1f6714 100644 --- a/plugins/funind/glob_termops.ml +++ b/plugins/funind/glob_termops.ml @@ -586,28 +586,28 @@ let id_of_name = function | Names.Name x -> x (* TODO: finish Rec caes *) -let ids_of_rawterm c = - let rec ids_of_rawterm acc c = +let ids_of_glob_constr c = + let rec ids_of_glob_constr acc c = let idof = id_of_name in match c with | GVar (_,id) -> id::acc | GApp (loc,g,args) -> - ids_of_rawterm [] g @ List.flatten (List.map (ids_of_rawterm []) args) @ acc - | GLambda (loc,na,k,ty,c) -> idof na :: ids_of_rawterm [] ty @ ids_of_rawterm [] c @ acc - | GProd (loc,na,k,ty,c) -> idof na :: ids_of_rawterm [] ty @ ids_of_rawterm [] c @ acc - | GLetIn (loc,na,b,c) -> idof na :: ids_of_rawterm [] b @ ids_of_rawterm [] c @ acc - | GCast (loc,c,CastConv(k,t)) -> ids_of_rawterm [] c @ ids_of_rawterm [] t @ acc - | GCast (loc,c,CastCoerce) -> ids_of_rawterm [] c @ acc - | GIf (loc,c,(na,po),b1,b2) -> ids_of_rawterm [] c @ ids_of_rawterm [] b1 @ ids_of_rawterm [] b2 @ acc + ids_of_glob_constr [] g @ List.flatten (List.map (ids_of_glob_constr []) args) @ acc + | GLambda (loc,na,k,ty,c) -> idof na :: ids_of_glob_constr [] ty @ ids_of_glob_constr [] c @ acc + | GProd (loc,na,k,ty,c) -> idof na :: ids_of_glob_constr [] ty @ ids_of_glob_constr [] c @ acc + | GLetIn (loc,na,b,c) -> idof na :: ids_of_glob_constr [] b @ ids_of_glob_constr [] c @ acc + | GCast (loc,c,CastConv(k,t)) -> ids_of_glob_constr [] c @ ids_of_glob_constr [] t @ acc + | GCast (loc,c,CastCoerce) -> ids_of_glob_constr [] c @ acc + | GIf (loc,c,(na,po),b1,b2) -> ids_of_glob_constr [] c @ ids_of_glob_constr [] b1 @ ids_of_glob_constr [] b2 @ acc | GLetTuple (_,nal,(na,po),b,c) -> - List.map idof nal @ ids_of_rawterm [] b @ ids_of_rawterm [] c @ acc + List.map idof nal @ ids_of_glob_constr [] b @ ids_of_glob_constr [] c @ acc | GCases (loc,sty,rtntypopt,tml,brchl) -> - List.flatten (List.map (fun (_,idl,patl,c) -> idl @ ids_of_rawterm [] c) brchl) + List.flatten (List.map (fun (_,idl,patl,c) -> idl @ ids_of_glob_constr [] c) brchl) | GRec _ -> failwith "Fix inside a constructor branch" | (GSort _ | GHole _ | GRef _ | GEvar _ | GPatVar _ | GDynamic _) -> [] in (* build the set *) - List.fold_left (fun acc x -> Idset.add x acc) Idset.empty (ids_of_rawterm [] c) + List.fold_left (fun acc x -> Idset.add x acc) Idset.empty (ids_of_glob_constr [] c) diff --git a/plugins/funind/glob_termops.mli b/plugins/funind/glob_termops.mli index b6c407a24..3afb86298 100644 --- a/plugins/funind/glob_termops.mli +++ b/plugins/funind/glob_termops.mli @@ -23,7 +23,7 @@ val mkRLambda : Names.name * glob_constr * glob_constr -> glob_constr val mkRProd : Names.name * glob_constr * glob_constr -> glob_constr val mkRLetIn : Names.name * glob_constr * glob_constr -> glob_constr val mkRCases : glob_constr option * tomatch_tuples * cases_clauses -> glob_constr -val mkRSort : rawsort -> glob_constr +val mkRSort : glob_sort -> glob_constr val mkRHole : unit -> glob_constr (* we only build Evd.BinderType Anonymous holes *) val mkRCast : glob_constr* glob_constr -> glob_constr (* @@ -115,10 +115,10 @@ val eq_cases_pattern : cases_pattern -> cases_pattern -> bool val ids_of_pat : cases_pattern -> Names.Idset.t (* TODO: finish this function (Fix not treated) *) -val ids_of_rawterm: glob_constr -> Names.Idset.t +val ids_of_glob_constr: glob_constr -> Names.Idset.t (* - removing let_in construction in a rawterm + removing let_in construction in a glob_constr *) val zeta_normalize : Glob_term.glob_constr -> Glob_term.glob_constr diff --git a/plugins/funind/invfun.ml b/plugins/funind/invfun.ml index 4e5fb953d..426b496dd 100644 --- a/plugins/funind/invfun.ml +++ b/plugins/funind/invfun.ml @@ -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,Glob_term.RType None) funs)) + (make_scheme (array_map_to_list (fun const -> const,Glob_term.GType None) funs)) ) in let proving_tac = diff --git a/plugins/funind/merge.ml b/plugins/funind/merge.ml index 7c32c1d20..4eedf8dc2 100644 --- a/plugins/funind/merge.ml +++ b/plugins/funind/merge.ml @@ -381,11 +381,11 @@ let build_raw_params prms_decl avoid = let _ = prNamedRConstr "RAWDUMMY" dummy_glob_constr in let res,_ = glob_decompose_prod dummy_glob_constr in let comblist = List.combine prms_decl res in - comblist, res , (avoid @ (Idset.elements (ids_of_rawterm dummy_glob_constr))) + comblist, res , (avoid @ (Idset.elements (ids_of_glob_constr dummy_glob_constr))) *) let ids_of_rawlist avoid rawl = - List.fold_left Idset.union avoid (List.map ids_of_rawterm rawl) + List.fold_left Idset.union avoid (List.map ids_of_glob_constr rawl) @@ -463,7 +463,7 @@ let shift_linked_params mib1 mib2 (lnk1:linked_var array) (lnk2:linked_var array ([],[],[],[]) arity_ctxt in (* let arity_ctxt2 = build_raw_params oib2.mind_arity_ctxt - (Idset.elements (ids_of_rawterm oib1.mind_arity_ctxt)) in*) + (Idset.elements (ids_of_glob_constr oib1.mind_arity_ctxt)) in*) let recprms1,otherprms1,args1,funresprms1 = bldprms (List.rev oib1.mind_arity_ctxt) mlnk1 in let _ = prstr "\n\n\n" in let recprms2,otherprms2,args2,funresprms2 = bldprms (List.rev oib2.mind_arity_ctxt) mlnk2 in @@ -756,7 +756,7 @@ let merge_constructor_id id1 id2 shift:identifier = (** [merge_constructors lnk shift avoid] merges the two list of - constructor [(name*type)]. These are translated to rawterms + constructor [(name*type)]. These are translated to glob_constr first, each of them having distinct var names. *) let rec merge_constructors (shift:merge_infos) (avoid:Idset.t) (typcstr1:(identifier * glob_constr) list) @@ -816,7 +816,7 @@ let rec merge_mutual_inductive_body merge_inductive_body shift Idset.empty mib1.mind_packets.(0) mib2.mind_packets.(0) -let rawterm_to_constr_expr x = (* build a constr_expr from a glob_constr *) +let glob_constr_to_constr_expr x = (* build a constr_expr from a glob_constr *) Flags.with_option Flags.raw_print (Constrextern.extern_glob_type Idset.empty) x let merge_rec_params_and_arity prms1 prms2 shift (concl:constr) = @@ -827,7 +827,7 @@ let merge_rec_params_and_arity prms1 prms2 shift (concl:constr) = let _ = prstr "param :" in let _ = prNamedRConstr (string_of_name nme) tp in let _ = prstr " ; " in - let typ = rawterm_to_constr_expr tp in + let typ = glob_constr_to_constr_expr tp in LocalRawAssum ([(dummy_loc,nme)], Topconstr.default_binder_kind, typ) :: acc) [] params in let concl = Constrextern.extern_constr false (Global.env()) concl in @@ -844,18 +844,18 @@ let merge_rec_params_and_arity prms1 prms2 shift (concl:constr) = -(** [rawterm_list_to_inductive_expr ident rawlist] returns the +(** [glob_constr_list_to_inductive_expr ident rawlist] returns the induct_expr corresponding to the the list of constructor types [rawlist], named ident. FIXME: params et cstr_expr (arity) *) -let rawterm_list_to_inductive_expr prms1 prms2 mib1 mib2 shift +let glob_constr_list_to_inductive_expr prms1 prms2 mib1 mib2 shift (rawlist:(identifier * glob_constr) list) = let lident = dummy_loc, shift.ident in let bindlist , cstr_expr = (* params , arities *) merge_rec_params_and_arity prms1 prms2 shift mkSet in let lcstor_expr : (bool * (lident * constr_expr)) list = List.map (* zeta_normalize t ? *) - (fun (id,t) -> false, ((dummy_loc,id),rawterm_to_constr_expr t)) + (fun (id,t) -> false, ((dummy_loc,id),glob_constr_to_constr_expr t)) rawlist in lident , bindlist , Some cstr_expr , lcstor_expr @@ -901,7 +901,7 @@ let merge_inductive (ind1: inductive) (ind2: inductive) recprms1=prms1; recprms1=prms1; } in *) - let indexpr = rawterm_list_to_inductive_expr prms1 prms2 mib1 mib2 shift_prm rawlist in + let indexpr = glob_constr_list_to_inductive_expr prms1 prms2 mib1 mib2 shift_prm rawlist in (* Declare inductive *) let indl,_,_ = Command.extract_mutual_inductive_declaration_components [(indexpr,[])] in let mie,impls = Command.interp_mutual_inductive indl [] true (* means: not coinductive *) in diff --git a/plugins/quote/quote.ml b/plugins/quote/quote.ml index 27f2292e3..41d92b233 100644 --- a/plugins/quote/quote.ml +++ b/plugins/quote/quote.ml @@ -470,7 +470,7 @@ Just testing ... #use "include.ml";; open Quote;; -let r = raw_constr_of_string;; +let r = glob_constr_of_string;; let ivs = { normal_lhs_rhs = diff --git a/plugins/subtac/subtac_cases.ml b/plugins/subtac/subtac_cases.ml index 4dfdc5875..4f8344745 100644 --- a/plugins/subtac/subtac_cases.ml +++ b/plugins/subtac/subtac_cases.ml @@ -155,22 +155,22 @@ let feed_history arg = function (* This is for non exhaustive error message *) -let rec rawpattern_of_partial_history args2 = function +let rec glob_pattern_of_partial_history args2 = function | Continuation (n, args1, h) -> let args3 = make_anonymous_patvars (n - (List.length args2)) in - build_rawpattern (List.rev_append args1 (args2@args3)) h + build_glob_pattern (List.rev_append args1 (args2@args3)) h | Result pl -> pl -and build_rawpattern args = function +and build_glob_pattern args = function | Top -> args | MakeAlias (AliasLeaf, rh) -> assert (args = []); - rawpattern_of_partial_history [PatVar (dummy_loc, Anonymous)] rh + glob_pattern_of_partial_history [PatVar (dummy_loc, Anonymous)] rh | MakeAlias (AliasConstructor pci, rh) -> - rawpattern_of_partial_history + glob_pattern_of_partial_history [PatCstr (dummy_loc, pci, args, Anonymous)] rh -let complete_history = rawpattern_of_partial_history [] +let complete_history = glob_pattern_of_partial_history [] (* This is to build glued pattern-matching history and alias bodies *) diff --git a/plugins/subtac/subtac_pretyping.ml b/plugins/subtac/subtac_pretyping.ml index c7924261a..7c0d12325 100644 --- a/plugins/subtac/subtac_pretyping.ml +++ b/plugins/subtac/subtac_pretyping.ml @@ -114,14 +114,14 @@ let subtac_process ?(is_type=false) env isevars id bl c tycon = | Some t -> let t = Topconstr.prod_constr_expr t bl in let t = coqintern_type !isevars env t in - let imps = Implicit_quantifiers.implicits_of_rawterm t in + let imps = Implicit_quantifiers.implicits_of_glob_constr t in let coqt, ttyp = interp env isevars t empty_tycon in mk_tycon coqt, Some imps in let c = coqintern_constr !isevars env c in let imps = match imps with | Some i -> i - | None -> Implicit_quantifiers.implicits_of_rawterm ~with_products:is_type c + | None -> Implicit_quantifiers.implicits_of_glob_constr ~with_products:is_type c in let coqc, ctyp = interp env isevars c tycon in let evm = non_instanciated_map env isevars !isevars in diff --git a/plugins/subtac/subtac_pretyping_F.ml b/plugins/subtac/subtac_pretyping_F.ml index b1c4101ce..28bf6e64d 100644 --- a/plugins/subtac/subtac_pretyping_F.ml +++ b/plugins/subtac/subtac_pretyping_F.ml @@ -160,8 +160,8 @@ module SubtacPretyping_F (Coercion : Coercion.S) = struct make_judge c (Retyping.get_type_of env Evd.empty c) let pretype_sort = function - | RProp c -> judge_of_prop_contents c - | RType _ -> judge_of_new_Type () + | GProp c -> judge_of_prop_contents c + | GType _ -> judge_of_new_Type () let split_tycon_lam loc env evd tycon = let rec real_split evd c = @@ -216,7 +216,7 @@ module SubtacPretyping_F (Coercion : Coercion.S) = struct inh_conv_coerce_to_tycon loc env evdref j tycon | GPatVar (loc,(someta,n)) -> - anomaly "Found a pattern variable in a rawterm to type" + anomaly "Found a pattern variable in a glob_constr to type" | GHole (loc,k) -> let ty = @@ -257,7 +257,7 @@ module SubtacPretyping_F (Coercion : Coercion.S) = struct in push_rec_types (names,marked_ftys,[||]) env in - let fixi = match fixkind with RFix (vn, i) -> i | RCoFix i -> i in + let fixi = match fixkind with GFix (vn, i) -> i | GCoFix i -> i in let vdefj = array_map2_i (fun i ctxt def -> @@ -284,7 +284,7 @@ module SubtacPretyping_F (Coercion : Coercion.S) = struct let ftys = Array.map (nf_evar !evdref) ftys in let fdefs = Array.map (fun x -> nf_evar !evdref (j_val x)) vdefj in let fixj = match fixkind with - | RFix (vn,i) -> + | GFix (vn,i) -> (* First, let's find the guard indexes. *) (* If recursive argument was not given by user, we try all args. An earlier approach was to look only for inductive arguments, @@ -300,7 +300,7 @@ module SubtacPretyping_F (Coercion : Coercion.S) = struct let fixdecls = (names,ftys,fdefs) in let indexes = search_guard loc env possible_indexes fixdecls in make_judge (mkFix ((indexes,i),fixdecls)) ftys.(i) - | RCoFix i -> + | GCoFix i -> let cofix = (i,(names,ftys,fdefs)) in (try check_cofix env cofix with e -> Loc.raise loc e); make_judge (mkCoFix cofix) ftys.(i) in diff --git a/pretyping/cases.ml b/pretyping/cases.ml index 6abcd0314..8e0d28fbf 100644 --- a/pretyping/cases.ml +++ b/pretyping/cases.ml @@ -196,22 +196,22 @@ let feed_history arg = function (* This is for non exhaustive error message *) -let rec rawpattern_of_partial_history args2 = function +let rec glob_pattern_of_partial_history args2 = function | Continuation (n, args1, h) -> let args3 = make_anonymous_patvars (n - (List.length args2)) in - build_rawpattern (List.rev_append args1 (args2@args3)) h + build_glob_pattern (List.rev_append args1 (args2@args3)) h | Result pl -> pl -and build_rawpattern args = function +and build_glob_pattern args = function | Top -> args | MakeAlias (AliasLeaf, rh) -> assert (args = []); - rawpattern_of_partial_history [PatVar (dummy_loc, Anonymous)] rh + glob_pattern_of_partial_history [PatVar (dummy_loc, Anonymous)] rh | MakeAlias (AliasConstructor pci, rh) -> - rawpattern_of_partial_history + glob_pattern_of_partial_history [PatCstr (dummy_loc, pci, args, Anonymous)] rh -let complete_history = rawpattern_of_partial_history [] +let complete_history = glob_pattern_of_partial_history [] (* This is to build glued pattern-matching history and alias bodies *) diff --git a/pretyping/detyping.ml b/pretyping/detyping.ml index 4ff4cd333..106629d2b 100644 --- a/pretyping/detyping.ml +++ b/pretyping/detyping.ml @@ -357,8 +357,8 @@ let detype_case computable detype detype_eqns testdep avoid data p c bl = GCases (dl,tag,pred,[tomatch,(alias,aliastyp)],eqnl) let detype_sort = function - | Prop c -> RProp c - | Type u -> RType (Some u) + | Prop c -> GProp c + | Type u -> GType (Some u) type binder_kind = BProd | BLambda | BLetIn @@ -424,7 +424,7 @@ and detype_fix isgoal avoid env (vn,_ as nvn) (names,tys,bodies) = let v = array_map3 (fun c t i -> share_names isgoal (i+1) [] def_avoid def_env c (lift n t)) bodies tys vn in - GRec(dl,RFix (Array.map (fun i -> Some i, RStructRec) (fst nvn), snd nvn),Array.of_list (List.rev lfi), + GRec(dl,GFix (Array.map (fun i -> Some i, GStructRec) (fst nvn), snd nvn),Array.of_list (List.rev lfi), Array.map (fun (bl,_,_) -> bl) v, Array.map (fun (_,_,ty) -> ty) v, Array.map (fun (_,bd,_) -> bd) v) @@ -440,7 +440,7 @@ and detype_cofix isgoal avoid env n (names,tys,bodies) = let v = array_map2 (fun c t -> share_names isgoal 0 [] def_avoid def_env c (lift ntys t)) bodies tys in - GRec(dl,RCoFix n,Array.of_list (List.rev lfi), + GRec(dl,GCoFix n,Array.of_list (List.rev lfi), Array.map (fun (bl,_,_) -> bl) v, Array.map (fun (_,_,ty) -> ty) v, Array.map (fun (_,bd,_) -> bd) v) diff --git a/pretyping/detyping.mli b/pretyping/detyping.mli index fd16c0013..ff98f747e 100644 --- a/pretyping/detyping.mli +++ b/pretyping/detyping.mli @@ -34,7 +34,7 @@ val detype_case : identifier list -> inductive * case_style * int * int array * int -> 'a option -> 'a -> 'a array -> glob_constr -val detype_sort : sorts -> rawsort +val detype_sort : sorts -> glob_sort val detype_rel_context : constr option -> identifier list -> names_context -> rel_context -> glob_decl list diff --git a/pretyping/glob_term.ml b/pretyping/glob_term.ml index deba9a257..b973a24f7 100644 --- a/pretyping/glob_term.ml +++ b/pretyping/glob_term.ml @@ -30,7 +30,7 @@ let cases_pattern_loc = function type patvar = identifier -type rawsort = RProp of Term.contents | RType of Univ.universe option +type glob_sort = GProp of Term.contents | GType of Univ.universe option type binding_kind = Lib.binding_kind = Explicit | Implicit @@ -64,18 +64,18 @@ type glob_constr = | GIf of loc * glob_constr * (name * glob_constr option) * glob_constr * glob_constr | GRec of loc * fix_kind * identifier array * glob_decl list array * glob_constr array * glob_constr array - | GSort of loc * rawsort + | GSort of loc * glob_sort | GHole of (loc * hole_kind) | GCast of loc * glob_constr * glob_constr cast_type | GDynamic of loc * Dyn.t and glob_decl = name * binding_kind * glob_constr option * glob_constr -and fix_recursion_order = RStructRec | RWfRec of glob_constr | RMeasureRec of glob_constr * glob_constr option +and fix_recursion_order = GStructRec | GWfRec of glob_constr | GMeasureRec of glob_constr * glob_constr option and fix_kind = - | RFix of ((int option * fix_recursion_order) array * int) - | RCoFix of int + | GFix of ((int option * fix_recursion_order) array * int) + | GCoFix of int and predicate_pattern = name * (loc * inductive * int * name list) option @@ -366,7 +366,7 @@ let glob_constr_of_closed_cases_pattern = function (**********************************************************************) (* Reduction expressions *) -type 'a raw_red_flag = { +type 'a glob_red_flag = { rBeta : bool; rIota : bool; rZeta : bool; @@ -392,8 +392,8 @@ type ('a,'b,'c) red_expr_gen = | Red of bool | Hnf | Simpl of 'c with_occurrences option - | Cbv of 'b raw_red_flag - | Lazy of 'b raw_red_flag + | Cbv of 'b glob_red_flag + | Lazy of 'b glob_red_flag | Unfold of 'b with_occurrences list | Fold of 'a list | Pattern of 'a with_occurrences list diff --git a/pretyping/glob_term.mli b/pretyping/glob_term.mli index 95305d58c..4e11221d8 100644 --- a/pretyping/glob_term.mli +++ b/pretyping/glob_term.mli @@ -31,7 +31,7 @@ val cases_pattern_loc : cases_pattern -> loc type patvar = identifier -type rawsort = RProp of Term.contents | RType of Univ.universe option +type glob_sort = GProp of Term.contents | GType of Univ.universe option type binding_kind = Lib.binding_kind = Explicit | Implicit @@ -65,18 +65,18 @@ type glob_constr = | GIf of loc * glob_constr * (name * glob_constr option) * glob_constr * glob_constr | GRec of loc * fix_kind * identifier array * glob_decl list array * glob_constr array * glob_constr array - | GSort of loc * rawsort + | GSort of loc * glob_sort | GHole of (loc * Evd.hole_kind) | GCast of loc * glob_constr * glob_constr cast_type | GDynamic of loc * Dyn.t and glob_decl = name * binding_kind * glob_constr option * glob_constr -and fix_recursion_order = RStructRec | RWfRec of glob_constr | RMeasureRec of glob_constr * glob_constr option +and fix_recursion_order = GStructRec | GWfRec of glob_constr | GMeasureRec of glob_constr * glob_constr option and fix_kind = - | RFix of ((int option * fix_recursion_order) array * int) - | RCoFix of int + | GFix of ((int option * fix_recursion_order) array * int) + | GCoFix of int and predicate_pattern = name * (loc * inductive * int * name list) option @@ -120,7 +120,7 @@ val glob_constr_of_closed_cases_pattern : cases_pattern -> name * glob_constr (** {6 Reduction expressions} *) -type 'a raw_red_flag = { +type 'a glob_red_flag = { rBeta : bool; rIota : bool; rZeta : bool; @@ -128,7 +128,7 @@ type 'a raw_red_flag = { rConst : 'a list } -val all_flags : 'a raw_red_flag +val all_flags : 'a glob_red_flag type 'a or_var = ArgArg of 'a | ArgVar of identifier located @@ -145,8 +145,8 @@ type ('a,'b,'c) red_expr_gen = | Red of bool | Hnf | Simpl of 'c with_occurrences option - | Cbv of 'b raw_red_flag - | Lazy of 'b raw_red_flag + | Cbv of 'b glob_red_flag + | Lazy of 'b glob_red_flag | Unfold of 'b with_occurrences list | Fold of 'a list | Pattern of 'a with_occurrences list diff --git a/pretyping/matching.ml b/pretyping/matching.ml index fc56f31d3..1facb7c7a 100644 --- a/pretyping/matching.ml +++ b/pretyping/matching.ml @@ -173,9 +173,9 @@ let matches_core convert allow_partial_app allow_bound_rels pat c = | PRel n1, Rel n2 when n1 = n2 -> subst - | PSort (RProp c1), Sort (Prop c2) when c1 = c2 -> subst + | PSort (GProp c1), Sort (Prop c2) when c1 = c2 -> subst - | PSort (RType _), Sort (Type _) -> subst + | PSort (GType _), Sort (Type _) -> subst | PApp (p, [||]), _ -> sorec stk subst p t diff --git a/pretyping/pattern.ml b/pretyping/pattern.ml index 19c5d156a..50dd413c6 100644 --- a/pretyping/pattern.ml +++ b/pretyping/pattern.ml @@ -36,7 +36,7 @@ type constr_pattern = | PLambda of name * constr_pattern * constr_pattern | PProd of name * constr_pattern * constr_pattern | PLetIn of name * constr_pattern * constr_pattern - | PSort of rawsort + | PSort of glob_sort | PMeta of patvar option | PIf of constr_pattern * constr_pattern * constr_pattern | PCase of (case_style * int array * inductive option * (int * int) option) @@ -92,8 +92,8 @@ let pattern_of_constr sigma t = | Rel n -> PRel n | Meta n -> PMeta (Some (id_of_string ("META" ^ string_of_int n))) | Var id -> PVar id - | Sort (Prop c) -> PSort (RProp c) - | Sort (Type _) -> PSort (RType None) + | Sort (Prop c) -> PSort (GProp c) + | Sort (Type _) -> PSort (GType None) | Cast (c,_,_) -> pattern_of_constr c | LetIn (na,c,_,b) -> PLetIn (na,pattern_of_constr c,pattern_of_constr b) | Prod (na,c,b) -> PProd (na,pattern_of_constr c,pattern_of_constr b) @@ -300,7 +300,7 @@ let rec pat_of_raw metas vars = function | (_,_,[PatCstr(_,(ind,_),_,_)],_)::_ -> Some ind | _ -> None in let cbrs = - Array.init (List.length brs) (pat_of_raw_branch loc metas vars ind brs) + Array.init (List.length brs) (pat_of_glob_branch loc metas vars ind brs) in let cstr_nargs,brs = (Array.map fst cbrs, Array.map snd cbrs) in PCase ((sty,cstr_nargs,ind,ind_nargs), pred, @@ -310,7 +310,7 @@ let rec pat_of_raw metas vars = function let loc = loc_of_glob_constr r in user_err_loc (loc,"pattern_of_glob_constr", Pp.str"Non supported pattern.") -and pat_of_raw_branch loc metas vars ind brs i = +and pat_of_glob_branch loc metas vars ind brs i = let bri = List.filter (function (_,_,[PatCstr(_,c,lv,Anonymous)],_) -> snd c = i+1 diff --git a/pretyping/pattern.mli b/pretyping/pattern.mli index b25637de9..23de67598 100644 --- a/pretyping/pattern.mli +++ b/pretyping/pattern.mli @@ -70,7 +70,7 @@ type constr_pattern = | PLambda of name * constr_pattern * constr_pattern | PProd of name * constr_pattern * constr_pattern | PLetIn of name * constr_pattern * constr_pattern - | PSort of rawsort + | PSort of glob_sort | PMeta of patvar option | PIf of constr_pattern * constr_pattern * constr_pattern | PCase of (case_style * int array * inductive option * (int * int) option) diff --git a/pretyping/pretype_errors.ml b/pretyping/pretype_errors.ml index b33157414..c0fa62048 100644 --- a/pretyping/pretype_errors.ml +++ b/pretyping/pretype_errors.ml @@ -183,7 +183,7 @@ let error_unexpected_type_loc loc env sigma actty expty = let error_not_product_loc loc env sigma c = raise_pretype_error (loc, env, sigma, NotProduct c) -(*s Error in conversion from AST to rawterms *) +(*s Error in conversion from AST to glob_constr *) let error_var_not_found_loc loc s = raise_pretype_error (loc, empty_env, Evd.empty, VarNotFound s) diff --git a/pretyping/pretype_errors.mli b/pretyping/pretype_errors.mli index 11722bee2..b55802044 100644 --- a/pretyping/pretype_errors.mli +++ b/pretyping/pretype_errors.mli @@ -123,6 +123,6 @@ val error_unexpected_type_loc : val error_not_product_loc : loc -> env -> Evd.evar_map -> constr -> 'b -(** {6 Error in conversion from AST to rawterms } *) +(** {6 Error in conversion from AST to glob_constr } *) val error_var_not_found_loc : loc -> identifier -> 'b diff --git a/pretyping/pretyping.ml b/pretyping/pretyping.ml index baa783d0c..a2fb8ea12 100644 --- a/pretyping/pretyping.ml +++ b/pretyping/pretyping.ml @@ -93,13 +93,13 @@ let ((constr_in : constr -> Dyn.t), (** Miscellaneous interpretation functions *) let interp_sort = function - | RProp c -> Prop c - | RType _ -> new_Type_sort () + | GProp c -> Prop c + | GType _ -> new_Type_sort () let interp_elimination_sort = function - | RProp Null -> InProp - | RProp Pos -> InSet - | RType _ -> InType + | GProp Null -> InProp + | GProp Pos -> InSet + | GType _ -> InType module type S = sig @@ -122,7 +122,7 @@ sig (* More general entry point with evars from ltac *) (* Generic call to the interpreter from glob_constr to constr, failing - unresolved holes in the rawterm cannot be instantiated. + unresolved holes in the glob_constr cannot be instantiated. In [understand_ltac expand_evars sigma env ltac_env constraint c], @@ -293,8 +293,8 @@ module Pretyping_F (Coercion : Coercion.S) = struct make_judge c (Retyping.get_type_of env Evd.empty c) let pretype_sort = function - | RProp c -> judge_of_prop_contents c - | RType _ -> judge_of_new_Type () + | GProp c -> judge_of_prop_contents c + | GType _ -> judge_of_new_Type () exception Found of fixpoint @@ -381,7 +381,7 @@ module Pretyping_F (Coercion : Coercion.S) = struct let ftys = Array.map (nf_evar !evdref) ftys in let fdefs = Array.map (fun x -> nf_evar !evdref (j_val x)) vdefj in let fixj = match fixkind with - | RFix (vn,i) -> + | GFix (vn,i) -> (* First, let's find the guard indexes. *) (* If recursive argument was not given by user, we try all args. An earlier approach was to look only for inductive arguments, @@ -397,7 +397,7 @@ module Pretyping_F (Coercion : Coercion.S) = struct let fixdecls = (names,ftys,fdefs) in let indexes = search_guard loc env possible_indexes fixdecls in make_judge (mkFix ((indexes,i),fixdecls)) ftys.(i) - | RCoFix i -> + | GCoFix i -> let cofix = (i,(names,ftys,fdefs)) in (try check_cofix env cofix with e -> Loc.raise loc e); make_judge (mkCoFix cofix) ftys.(i) in diff --git a/pretyping/pretyping.mli b/pretyping/pretyping.mli index 70e1a22fb..e1f79f36c 100644 --- a/pretyping/pretyping.mli +++ b/pretyping/pretyping.mli @@ -53,7 +53,7 @@ sig (** More general entry point with evars from ltac *) (** Generic call to the interpreter from glob_constr to constr, failing - unresolved holes in the rawterm cannot be instantiated. + unresolved holes in the glob_constr cannot be instantiated. In [understand_ltac expand_evars sigma env ltac_env constraint c], @@ -114,6 +114,6 @@ module Default : S val constr_in : constr -> Dyn.t val constr_out : Dyn.t -> constr -val interp_sort : rawsort -> sorts -val interp_elimination_sort : rawsort -> sorts_family +val interp_sort : glob_sort -> sorts +val interp_elimination_sort : glob_sort -> sorts_family diff --git a/proofs/tacexpr.ml b/proofs/tacexpr.ml index 428c67475..b37460e48 100644 --- a/proofs/tacexpr.ml +++ b/proofs/tacexpr.ml @@ -27,7 +27,7 @@ type split_flag = bool (* true = exists false = split *) type hidden_flag = bool (* true = internal use false = user-level *) type letin_flag = bool (* true = use local def false = use Leibniz *) -type raw_red_flag = +type glob_red_flag = | FBeta | FIota | FZeta diff --git a/tactics/extratactics.ml4 b/tactics/extratactics.ml4 index 6377eafd9..f774df5de 100644 --- a/tactics/extratactics.ml4 +++ b/tactics/extratactics.ml4 @@ -324,7 +324,7 @@ 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 (Glob_term.RProp Term.Null) false inv_clear_tac ] + -> [ add_inversion_lemma_exn na c (Glob_term.GProp Term.Null) false inv_clear_tac ] END open Term @@ -335,7 +335,7 @@ VERNAC COMMAND EXTEND DeriveInversion -> [ add_inversion_lemma_exn na c s false inv_tac ] | [ "Derive" "Inversion" ident(na) "with" constr(c) ] - -> [ add_inversion_lemma_exn na c (RProp Null) false inv_tac ] + -> [ add_inversion_lemma_exn na c (GProp Null) false inv_tac ] | [ "Derive" "Inversion" ident(na) hyp(id) ] -> [ inversion_lemma_from_goal 1 na id Term.prop_sort false inv_tac ] diff --git a/tactics/leminv.mli b/tactics/leminv.mli index 1ac9b4d6f..233aeba3a 100644 --- a/tactics/leminv.mli +++ b/tactics/leminv.mli @@ -15,5 +15,5 @@ val inversion_lemma_from_goal : int -> identifier -> identifier located -> sorts -> bool -> (identifier -> tactic) -> unit val add_inversion_lemma_exn : - identifier -> constr_expr -> rawsort -> bool -> (identifier -> tactic) -> + identifier -> constr_expr -> glob_sort -> bool -> (identifier -> tactic) -> unit 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 |