diff options
43 files changed, 351 insertions, 317 deletions
diff --git a/engine/eConstr.ml b/engine/eConstr.ml index 657285de2..7d4d17c63 100644 --- a/engine/eConstr.ml +++ b/engine/eConstr.ml @@ -131,6 +131,8 @@ let isCase sigma c = match kind sigma c with Case _ -> true | _ -> false let isProj sigma c = match kind sigma c with Proj _ -> true | _ -> false let isVarId sigma id c = match kind sigma c with Var id' -> Id.equal id id' | _ -> false +let isRelN sigma n c = + match kind sigma c with Rel n' -> Int.equal n n' | _ -> false let destRel sigma c = match kind sigma c with | Rel p -> p diff --git a/engine/eConstr.mli b/engine/eConstr.mli index d6b2113d2..83536d6f8 100644 --- a/engine/eConstr.mli +++ b/engine/eConstr.mli @@ -114,6 +114,7 @@ val isCase : Evd.evar_map -> t -> bool val isProj : Evd.evar_map -> t -> bool val isArity : Evd.evar_map -> t -> bool val isVarId : Evd.evar_map -> Id.t -> t -> bool +val isRelN : Evd.evar_map -> int -> t -> bool val destRel : Evd.evar_map -> t -> int val destMeta : Evd.evar_map -> t -> metavariable diff --git a/engine/engine.mllib b/engine/engine.mllib index c78f37a85..1b670d366 100644 --- a/engine/engine.mllib +++ b/engine/engine.mllib @@ -1,10 +1,10 @@ Logic_monad -Namegen Universes UState Evd Sigma EConstr +Namegen Termops Proofview_monad Evarutil diff --git a/engine/evarutil.ml b/engine/evarutil.ml index e94fd72f1..ce6d06f23 100644 --- a/engine/evarutil.ml +++ b/engine/evarutil.ml @@ -326,7 +326,7 @@ let push_var id (n, s) = let s = Int.Map.add n (EConstr.mkVar id) s in (succ n, s) -let push_rel_decl_to_named_context decl (subst, vsubst, avoid, nc) = +let push_rel_decl_to_named_context sigma decl (subst, vsubst, avoid, nc) = let open EConstr in let open Vars in let map_decl f d = @@ -354,7 +354,7 @@ let push_rel_decl_to_named_context decl (subst, vsubst, avoid, nc) = else (** id_of_name_using_hdchar only depends on the rel context which is empty here *) - next_ident_away (id_of_name_using_hdchar empty_env (EConstr.Unsafe.to_constr (RelDecl.get_type decl)) na) avoid + next_ident_away (id_of_name_using_hdchar empty_env sigma (RelDecl.get_type decl) na) avoid in match extract_if_neq id na with | Some id0 when not (is_section_variable id0) -> @@ -375,7 +375,7 @@ let push_rel_decl_to_named_context decl (subst, vsubst, avoid, nc) = let d = decl |> NamedDecl.of_rel_decl (fun _ -> id) |> map_decl (subst2 subst vsubst) in (push_var id subst, vsubst, Id.Set.add id avoid, d :: nc) -let push_rel_context_to_named_context env typ = +let push_rel_context_to_named_context env sigma typ = (* compute the instances relative to the named context and rel_context *) let open Context.Named.Declaration in let open EConstr in @@ -390,7 +390,7 @@ let push_rel_context_to_named_context env typ = (* with vars of the rel context *) (* We do keep the instances corresponding to local definition (see above) *) let (subst, vsubst, _, env) = - Context.Rel.fold_outside push_rel_decl_to_named_context + Context.Rel.fold_outside (fun d acc -> push_rel_decl_to_named_context sigma d acc) (rel_context env) ~init:(empty_csubst, [], avoid, named_context env) in (val_of_named_context env, subst2 subst vsubst typ, inst_rels@inst_vars, subst, vsubst) @@ -452,7 +452,7 @@ let new_evar_instance sign evd typ ?src ?filter ?candidates ?store ?naming ?prin (* [new_evar] declares a new existential in an env env with type typ *) (* Converting the env into the sign of the evar to define *) let new_evar env evd ?src ?filter ?candidates ?store ?naming ?principal typ = - let sign,typ',instance,subst,vsubst = push_rel_context_to_named_context env typ in + let sign,typ',instance,subst,vsubst = push_rel_context_to_named_context env (Sigma.to_evar_map evd) typ in let map c = subst2 subst vsubst c in let candidates = Option.map (fun l -> List.map map l) candidates in let instance = diff --git a/engine/evarutil.mli b/engine/evarutil.mli index 2da4f8043..da49d4e11 100644 --- a/engine/evarutil.mli +++ b/engine/evarutil.mli @@ -216,9 +216,9 @@ type ext_named_context = Id.Set.t * named_context val push_rel_decl_to_named_context : - rel_declaration -> ext_named_context -> ext_named_context + evar_map -> rel_declaration -> ext_named_context -> ext_named_context -val push_rel_context_to_named_context : Environ.env -> types -> +val push_rel_context_to_named_context : Environ.env -> evar_map -> types -> named_context_val * types * constr list * csubst * (identifier*constr) list val generalize_evar_over_rels : evar_map -> existential -> types * constr list diff --git a/engine/namegen.ml b/engine/namegen.ml index e56ec2877..7b7302957 100644 --- a/engine/namegen.ml +++ b/engine/namegen.ml @@ -15,12 +15,13 @@ open Util open Names open Term +open Environ +open EConstr open Vars open Nametab open Nameops open Libnames open Globnames -open Environ open Context.Rel.Declaration module RelDecl = Context.Rel.Declaration @@ -84,13 +85,20 @@ let is_section_variable id = (**********************************************************************) (* Generating "intuitive" names from its type *) -let head_name c = (* Find the head constant of a constr if any *) +let global_of_constr = function +| Const (c, _) -> ConstRef c +| Ind (i, _) -> IndRef i +| Construct (c, _) -> ConstructRef c +| Var id -> VarRef id +| _ -> assert false + +let head_name sigma c = (* Find the head constant of a constr if any *) let rec hdrec c = - match kind_of_term c with + match EConstr.kind sigma c with | Prod (_,_,c) | Lambda (_,_,c) | LetIn (_,_,_,c) | Cast (c,_,_) | App (c,_) -> hdrec c | Proj (kn,_) -> Some (Label.to_id (con_label (Projection.constant kn))) - | Const _ | Ind _ | Construct _ | Var _ -> + | Const _ | Ind _ | Construct _ | Var _ as c -> Some (basename_of_global (global_of_constr c)) | Fix ((_,i),(lna,_,_)) | CoFix (i,(lna,_,_)) -> Some (match lna.(i) with Name id -> id | _ -> assert false) @@ -105,9 +113,9 @@ let sort_hdchar = function | Prop(_) -> "P" | Type(_) -> "T" -let hdchar env c = +let hdchar env sigma c = let rec hdrec k c = - match kind_of_term c with + match EConstr.kind sigma c with | Prod (_,_,c) | Lambda (_,_,c) | LetIn (_,_,_,c) -> hdrec (k+1) c | Cast (c,_,_) | App (c,_) -> hdrec k c | Proj (kn,_) -> lowercase_first_char (Label.to_id (con_label (Projection.constant kn))) @@ -119,7 +127,7 @@ let hdchar env c = | Rel n -> (if n<=k then "p" (* the initial term is flexible product/function *) else - try match Environ.lookup_rel (n-k) env with + try match lookup_rel (n-k) env with | LocalAssum (Name id,_) | LocalDef (Name id,_,_) -> lowercase_first_char id | LocalAssum (Anonymous,t) | LocalDef (Anonymous,_,t) -> hdrec 0 (lift (n-k) t) with Not_found -> "y") @@ -131,41 +139,41 @@ let hdchar env c = in hdrec 0 c -let id_of_name_using_hdchar env a = function - | Anonymous -> Id.of_string (hdchar env a) +let id_of_name_using_hdchar env sigma a = function + | Anonymous -> Id.of_string (hdchar env sigma a) | Name id -> id -let named_hd env a = function - | Anonymous -> Name (Id.of_string (hdchar env a)) +let named_hd env sigma a = function + | Anonymous -> Name (Id.of_string (hdchar env sigma a)) | x -> x -let mkProd_name env (n,a,b) = mkProd (named_hd env a n, a, b) -let mkLambda_name env (n,a,b) = mkLambda (named_hd env a n, a, b) +let mkProd_name env sigma (n,a,b) = mkProd (named_hd env sigma a n, a, b) +let mkLambda_name env sigma (n,a,b) = mkLambda (named_hd env sigma a n, a, b) let lambda_name = mkLambda_name let prod_name = mkProd_name -let prod_create env (a,b) = mkProd (named_hd env a Anonymous, a, b) -let lambda_create env (a,b) = mkLambda (named_hd env a Anonymous, a, b) +let prod_create env sigma (a,b) = mkProd (named_hd env sigma a Anonymous, a, b) +let lambda_create env sigma (a,b) = mkLambda (named_hd env sigma a Anonymous, a, b) -let name_assumption env = function - | LocalAssum (na,t) -> LocalAssum (named_hd env t na, t) - | LocalDef (na,c,t) -> LocalDef (named_hd env c na, c, t) +let name_assumption env sigma = function + | LocalAssum (na,t) -> LocalAssum (named_hd env sigma t na, t) + | LocalDef (na,c,t) -> LocalDef (named_hd env sigma c na, c, t) -let name_context env hyps = +let name_context env sigma hyps = snd (List.fold_left (fun (env,hyps) d -> - let d' = name_assumption env d in (push_rel d' env, d' :: hyps)) + let d' = name_assumption env sigma d in (push_rel d' env, d' :: hyps)) (env,[]) (List.rev hyps)) -let mkProd_or_LetIn_name env b d = mkProd_or_LetIn (name_assumption env d) b -let mkLambda_or_LetIn_name env b d = mkLambda_or_LetIn (name_assumption env d)b +let mkProd_or_LetIn_name env sigma b d = mkProd_or_LetIn (name_assumption env sigma d) b +let mkLambda_or_LetIn_name env sigma b d = mkLambda_or_LetIn (name_assumption env sigma d) b -let it_mkProd_or_LetIn_name env b hyps = - it_mkProd_or_LetIn b (name_context env hyps) -let it_mkLambda_or_LetIn_name env b hyps = - it_mkLambda_or_LetIn b (name_context env hyps) +let it_mkProd_or_LetIn_name env sigma b hyps = + it_mkProd_or_LetIn b (name_context env sigma hyps) +let it_mkLambda_or_LetIn_name env sigma b hyps = + it_mkLambda_or_LetIn b (name_context env sigma hyps) (**********************************************************************) (* Fresh names *) @@ -185,10 +193,10 @@ let restart_subscript id = *** make_ident id (Some 0) *** but compatibility would be lost... *) forget_subscript id -let visible_ids (nenv, c) = +let visible_ids sigma (nenv, c) = let accu = ref (Refset_env.empty, Int.Set.empty, Id.Set.empty) in - let rec visible_ids n c = match kind_of_term c with - | Const _ | Ind _ | Construct _ | Var _ -> + let rec visible_ids n c = match EConstr.kind sigma c with + | Const _ | Ind _ | Construct _ | Var _ as c -> let (gseen, vseen, ids) = !accu in let g = global_of_constr c in if not (Refset_env.mem g gseen) then @@ -218,7 +226,7 @@ let visible_ids (nenv, c) = | _ -> ids in accu := (gseen, vseen, ids) - | _ -> Constr.iter_with_binders succ visible_ids n c + | _ -> EConstr.iter_with_binders sigma succ visible_ids n c in let () = visible_ids 1 c in let (_, _, ids) = !accu in @@ -228,9 +236,9 @@ let visible_ids (nenv, c) = (* 1- Looks for a fresh name for printing in cases pattern *) -let next_name_away_in_cases_pattern env_t na avoid = +let next_name_away_in_cases_pattern sigma env_t na avoid = let id = match na with Name id -> id | Anonymous -> default_dependent_ident in - let visible = visible_ids env_t in + let visible = visible_ids sigma env_t in let bad id = Id.List.mem id avoid || is_constructor id || Id.Set.mem id visible in next_ident_away_from id bad @@ -292,7 +300,7 @@ let next_name_away_with_default_using_types default na avoid t = let next_name_away = next_name_away_with_default default_non_dependent_string -let make_all_name_different env = +let make_all_name_different env sigma = (** FIXME: this is inefficient, but only used in printing *) let avoid = ref (Id.Set.elements (Context.Named.to_vars (named_context env))) in let sign = named_context_val env in @@ -300,7 +308,7 @@ let make_all_name_different env = let env0 = reset_with_named_context sign env in Context.Rel.fold_outside (fun decl newenv -> - let na = named_hd newenv (RelDecl.get_type decl) (RelDecl.get_name decl) in + let na = named_hd newenv sigma (RelDecl.get_type decl) (RelDecl.get_name decl) in let id = next_name_away na !avoid in avoid := id::!avoid; push_rel (RelDecl.set_name (Name id) decl) newenv) @@ -311,12 +319,12 @@ let make_all_name_different env = looks for name of same base with lower available subscript beyond current subscript *) -let next_ident_away_for_default_printing env_t id avoid = - let visible = visible_ids env_t in +let next_ident_away_for_default_printing sigma env_t id avoid = + let visible = visible_ids sigma env_t in let bad id = Id.List.mem id avoid || Id.Set.mem id visible in next_ident_away_from id bad -let next_name_away_for_default_printing env_t na avoid = +let next_name_away_for_default_printing sigma env_t na avoid = let id = match na with | Name id -> id | Anonymous -> @@ -324,7 +332,7 @@ let next_name_away_for_default_printing env_t na avoid = (* taken into account by the function compute_displayed_name_in; *) (* just in case, invent a valid name *) default_non_dependent_ident in - next_ident_away_for_default_printing env_t id avoid + next_ident_away_for_default_printing sigma env_t id avoid (**********************************************************************) (* Displaying terms avoiding bound variables clashes *) @@ -349,45 +357,45 @@ type renaming_flags = | RenamingForGoal | RenamingElsewhereFor of (Name.t list * constr) -let next_name_for_display flags = +let next_name_for_display sigma flags = match flags with - | RenamingForCasesPattern env_t -> next_name_away_in_cases_pattern env_t + | RenamingForCasesPattern env_t -> next_name_away_in_cases_pattern sigma env_t | RenamingForGoal -> next_name_away_in_goal - | RenamingElsewhereFor env_t -> next_name_away_for_default_printing env_t + | RenamingElsewhereFor env_t -> next_name_away_for_default_printing sigma env_t (* Remark: Anonymous var may be dependent in Evar's contexts *) -let compute_displayed_name_in flags avoid na c = +let compute_displayed_name_in sigma flags avoid na c = match na with - | Anonymous when noccurn 1 c -> + | Anonymous when noccurn sigma 1 c -> (Anonymous,avoid) | _ -> - let fresh_id = next_name_for_display flags na avoid in - let idopt = if noccurn 1 c then Anonymous else Name fresh_id in + let fresh_id = next_name_for_display sigma flags na avoid in + let idopt = if noccurn sigma 1 c then Anonymous else Name fresh_id in (idopt, fresh_id::avoid) -let compute_and_force_displayed_name_in flags avoid na c = +let compute_and_force_displayed_name_in sigma flags avoid na c = match na with - | Anonymous when noccurn 1 c -> + | Anonymous when noccurn sigma 1 c -> (Anonymous,avoid) | _ -> - let fresh_id = next_name_for_display flags na avoid in + let fresh_id = next_name_for_display sigma flags na avoid in (Name fresh_id, fresh_id::avoid) -let compute_displayed_let_name_in flags avoid na c = - let fresh_id = next_name_for_display flags na avoid in +let compute_displayed_let_name_in sigma flags avoid na c = + let fresh_id = next_name_for_display sigma flags na avoid in (Name fresh_id, fresh_id::avoid) -let rename_bound_vars_as_displayed avoid env c = +let rename_bound_vars_as_displayed sigma avoid env c = let rec rename avoid env c = - match kind_of_term c with + match EConstr.kind sigma c with | Prod (na,c1,c2) -> let na',avoid' = - compute_displayed_name_in + compute_displayed_name_in sigma (RenamingElsewhereFor (env,c2)) avoid na c2 in mkProd (na', c1, rename avoid' (na' :: env) c2) | LetIn (na,c1,t,c2) -> let na',avoid' = - compute_displayed_let_name_in + compute_displayed_let_name_in sigma (RenamingElsewhereFor (env,c2)) avoid na c2 in mkLetIn (na',c1,t, rename avoid' (na' :: env) c2) | Cast (c,k,t) -> mkCast (rename avoid env c, k,t) diff --git a/engine/namegen.mli b/engine/namegen.mli index 33ce9a34d..058b1c228 100644 --- a/engine/namegen.mli +++ b/engine/namegen.mli @@ -11,6 +11,8 @@ open Names open Term open Environ +open Evd +open EConstr (********************************************************************* Conventional default names *) @@ -26,27 +28,27 @@ val default_dependent_ident : Id.t (* "x" *) val lowercase_first_char : Id.t -> string val sort_hdchar : sorts -> string -val hdchar : env -> types -> string -val id_of_name_using_hdchar : env -> types -> Name.t -> Id.t -val named_hd : env -> types -> Name.t -> Name.t -val head_name : types -> Id.t option +val hdchar : env -> evar_map -> types -> string +val id_of_name_using_hdchar : env -> evar_map -> types -> Name.t -> Id.t +val named_hd : env -> evar_map -> types -> Name.t -> Name.t +val head_name : evar_map -> types -> Id.t option -val mkProd_name : env -> Name.t * types * types -> types -val mkLambda_name : env -> Name.t * types * constr -> constr +val mkProd_name : env -> evar_map -> Name.t * types * types -> types +val mkLambda_name : env -> evar_map -> Name.t * types * constr -> constr (** Deprecated synonyms of [mkProd_name] and [mkLambda_name] *) -val prod_name : env -> Name.t * types * types -> types -val lambda_name : env -> Name.t * types * constr -> constr +val prod_name : env -> evar_map -> Name.t * types * types -> types +val lambda_name : env -> evar_map -> Name.t * types * constr -> constr -val prod_create : env -> types * types -> constr -val lambda_create : env -> types * constr -> constr -val name_assumption : env -> Context.Rel.Declaration.t -> Context.Rel.Declaration.t -val name_context : env -> Context.Rel.t -> Context.Rel.t +val prod_create : env -> evar_map -> types * types -> constr +val lambda_create : env -> evar_map -> types * constr -> constr +val name_assumption : env -> evar_map -> rel_declaration -> rel_declaration +val name_context : env -> evar_map -> rel_context -> rel_context -val mkProd_or_LetIn_name : env -> types -> Context.Rel.Declaration.t -> types -val mkLambda_or_LetIn_name : env -> constr -> Context.Rel.Declaration.t -> constr -val it_mkProd_or_LetIn_name : env -> types -> Context.Rel.t -> types -val it_mkLambda_or_LetIn_name : env -> constr -> Context.Rel.t -> constr +val mkProd_or_LetIn_name : env -> evar_map -> types -> rel_declaration -> types +val mkLambda_or_LetIn_name : env -> evar_map -> constr -> rel_declaration -> constr +val it_mkProd_or_LetIn_name : env -> evar_map -> types -> rel_context -> types +val it_mkLambda_or_LetIn_name : env -> evar_map -> constr -> rel_context -> constr (********************************************************************* Fresh names *) @@ -98,16 +100,16 @@ type renaming_flags = | RenamingForGoal (** avoid all globals (as in intro) *) | RenamingElsewhereFor of (Name.t list * constr) -val make_all_name_different : env -> env +val make_all_name_different : env -> evar_map -> env val compute_displayed_name_in : - renaming_flags -> Id.t list -> Name.t -> constr -> Name.t * Id.t list + evar_map -> renaming_flags -> Id.t list -> Name.t -> constr -> Name.t * Id.t list val compute_and_force_displayed_name_in : - renaming_flags -> Id.t list -> Name.t -> constr -> Name.t * Id.t list + evar_map -> renaming_flags -> Id.t list -> Name.t -> constr -> Name.t * Id.t list val compute_displayed_let_name_in : - renaming_flags -> Id.t list -> Name.t -> constr -> Name.t * Id.t list + evar_map -> renaming_flags -> Id.t list -> Name.t -> constr -> Name.t * Id.t list val rename_bound_vars_as_displayed : - Id.t list -> Name.t list -> types -> types + evar_map -> Id.t list -> Name.t list -> types -> types (**********************************************************************) (* Naming strategy for arguments in Prop when eliminating inductive types *) diff --git a/engine/termops.ml b/engine/termops.ml index ff1a0d9de..d8e712abc 100644 --- a/engine/termops.ml +++ b/engine/termops.ml @@ -115,7 +115,7 @@ let pr_evar_suggested_name evk sigma = | _,Evar_kinds.GoalEvar -> Id.of_string "Goal" | _ -> let env = reset_with_named_context evi.evar_hyps (Global.env()) in - Namegen.id_of_name_using_hdchar env evi.evar_concl Anonymous + Namegen.id_of_name_using_hdchar env sigma (EConstr.of_constr evi.evar_concl) Anonymous in let names = EvMap.mapi base_id (undefined_map sigma) in let id = EvMap.find evk names in @@ -316,7 +316,7 @@ let print_env_short env = str "[" ++ pr_sequence pr_named_decl nc ++ str "]" ++ spc () ++ str "[" ++ pr_sequence pr_rel_decl rc ++ str "]" -let pr_evar_constraints pbs = +let pr_evar_constraints sigma pbs = let pr_evconstr (pbty, env, t1, t2) = let env = (** We currently allow evar instances to refer to anonymous de @@ -326,10 +326,10 @@ let pr_evar_constraints pbs = stop depending on anonymous variables, they can be used to indicate independency. Also, this depends on a strategy for naming/renaming. *) - Namegen.make_all_name_different env + Namegen.make_all_name_different env sigma in print_env_short env ++ spc () ++ str "|-" ++ spc () ++ - print_constr_env env Evd.empty (EConstr.of_constr t1) ++ spc () ++ + print_constr_env env sigma (EConstr.of_constr t1) ++ spc () ++ str (match pbty with | Reduction.CONV -> "==" | Reduction.CUMUL -> "<=") ++ @@ -346,7 +346,7 @@ let pr_evar_map_gen with_univs pr_evars sigma = if List.is_empty conv_pbs then mt () else str "CONSTRAINTS:" ++ brk (0, 1) ++ - pr_evar_constraints conv_pbs ++ fnl () + pr_evar_constraints sigma conv_pbs ++ fnl () and metas = if List.is_empty (Evd.meta_list sigma) then mt () else diff --git a/engine/termops.mli b/engine/termops.mli index 512bb05ff..0dd5d96fb 100644 --- a/engine/termops.mli +++ b/engine/termops.mli @@ -288,7 +288,7 @@ val pr_existential_key : evar_map -> evar -> Pp.std_ppcmds val pr_evar_suggested_name : existential_key -> evar_map -> Id.t val pr_evar_info : evar_info -> Pp.std_ppcmds -val pr_evar_constraints : evar_constraint list -> Pp.std_ppcmds +val pr_evar_constraints : evar_map -> evar_constraint list -> Pp.std_ppcmds val pr_evar_map : ?with_univs:bool -> int option -> evar_map -> Pp.std_ppcmds val pr_evar_map_filter : ?with_univs:bool -> (Evar.t -> evar_info -> bool) -> evar_map -> Pp.std_ppcmds diff --git a/interp/constrextern.ml b/interp/constrextern.ml index 3077231be..8debc06bb 100644 --- a/interp/constrextern.ml +++ b/interp/constrextern.ml @@ -953,6 +953,7 @@ let extern_constr_gen lax goal_concl_style scopt env sigma t = (* Not "goal_concl_style" means do alpha-conversion avoiding only *) (* those goal/section/rel variables that occurs in the subterm under *) (* consideration; see namegen.ml for further details *) + let t = EConstr.of_constr t in let avoid = if goal_concl_style then ids_of_context env else [] in let r = Detyping.detype ~lax:lax goal_concl_style avoid env sigma t in let vars = vars_of_env env in @@ -965,6 +966,7 @@ let extern_constr ?(lax=false) goal_concl_style env sigma t = extern_constr_gen lax goal_concl_style None env sigma t let extern_type goal_concl_style env sigma t = + let t = EConstr.of_constr t in let avoid = if goal_concl_style then ids_of_context env else [] in let r = Detyping.detype goal_concl_style avoid env sigma t in extern_glob_type (vars_of_env env) r @@ -1042,14 +1044,16 @@ let rec glob_of_pat env sigma = function | _ -> anomaly (Pp.str "PCase with non-trivial predicate but unknown inductive") in GCases (loc,RegularStyle,rtn,[glob_of_pat env sigma tm,indnames],mat) - | PFix f -> Detyping.detype_names false [] env (Global.env()) sigma (mkFix f) (** FIXME bad env *) - | PCoFix c -> Detyping.detype_names false [] env (Global.env()) sigma (mkCoFix c) + | PFix f -> Detyping.detype_names false [] env (Global.env()) sigma (EConstr.of_constr (mkFix f)) (** FIXME bad env *) + | PCoFix c -> Detyping.detype_names false [] env (Global.env()) sigma (EConstr.of_constr (mkCoFix c)) | PSort s -> GSort (loc,s) let extern_constr_pattern env sigma pat = extern true (None,[]) Id.Set.empty (glob_of_pat env sigma pat) let extern_rel_context where env sigma sign = + let sign = List.map (fun d -> Termops.map_rel_decl EConstr.of_constr d) sign in + let where = Option.map EConstr.of_constr where in let a = detype_rel_context where [] (names_of_rel_context env,env) sigma sign in let vars = vars_of_env env in let a = List.map (fun (p,bk,x,t) -> (Inl p,bk,x,t)) a in diff --git a/interp/constrintern.ml b/interp/constrintern.ml index 41e2e4e6f..bac97aa3f 100644 --- a/interp/constrintern.ml +++ b/interp/constrintern.ml @@ -1843,7 +1843,7 @@ let internalize globalenv env allow_patvar (_, ntnvars as lvar) c = (add_name match_acc (loc,x)) ((loc,x)::var_acc) | (LocalAssum (cano_name,ty) | LocalDef (cano_name,_,ty)) :: t, c::tt -> let fresh = - Namegen.next_name_away_with_default_using_types "iV" cano_name forbidden_names ty in + Namegen.next_name_away_with_default_using_types "iV" cano_name forbidden_names (EConstr.of_constr ty) in canonize_args t tt (fresh::forbidden_names) ((fresh,c)::match_acc) ((cases_pattern_loc c,Name fresh)::var_acc) | _ -> assert false in diff --git a/interp/notation_ops.ml b/interp/notation_ops.ml index 7dbd94aa7..549e8e787 100644 --- a/interp/notation_ops.ml +++ b/interp/notation_ops.ml @@ -441,6 +441,7 @@ let notation_constr_of_glob_constr nenv a = (* Substitution of kernel names, avoiding a list of bound identifiers *) let notation_constr_of_constr avoiding t = + let t = EConstr.of_constr t in let t = Detyping.detype false avoiding (Global.env()) Evd.empty t in let nenv = { ninterp_var_type = Id.Map.empty; diff --git a/interp/reserve.ml b/interp/reserve.ml index a4d4f4027..1565ba4a9 100644 --- a/interp/reserve.ml +++ b/interp/reserve.ml @@ -107,7 +107,9 @@ let constr_key c = let revert_reserved_type t = try + let t = EConstr.Unsafe.to_constr t in let reserved = KeyMap.find (constr_key t) !reserve_revtable in + let t = EConstr.of_constr t in let t = Detyping.detype false [] (Global.env()) Evd.empty t in (* pedrot: if [Notation_ops.match_notation_constr] may raise [Failure _] then I've introduced a bug... *) diff --git a/library/impargs.ml b/library/impargs.ml index 836568b89..a63264b66 100644 --- a/library/impargs.ml +++ b/library/impargs.ml @@ -228,10 +228,12 @@ let rec is_rigid_head t = match kind_of_term t with (* calcule la liste des arguments implicites *) -let find_displayed_name_in all avoid na (_,b as envnames_b) = +let find_displayed_name_in all avoid na (env, b) = + let b = EConstr.of_constr b in + let envnames_b = (env, b) in let flag = RenamingElsewhereFor envnames_b in - if all then compute_and_force_displayed_name_in flag avoid na b - else compute_displayed_name_in flag avoid na b + if all then compute_and_force_displayed_name_in Evd.empty flag avoid na b + else compute_displayed_name_in Evd.empty flag avoid na b let compute_implicits_gen strict strongly_strict revpat contextual all env t = let rigid = ref true in diff --git a/ltac/evar_tactics.ml b/ltac/evar_tactics.ml index 01cff94a8..5d3f6df03 100644 --- a/ltac/evar_tactics.ml +++ b/ltac/evar_tactics.ml @@ -88,14 +88,14 @@ let let_evar name typ = let env = Proofview.Goal.env gl in let sigma = ref sigma in let _ = Typing.e_sort_of env sigma typ in - let sigma = Sigma.Unsafe.of_evar_map !sigma in + let sigma = !sigma in let id = match name with | Names.Anonymous -> - let typ = EConstr.Unsafe.to_constr typ in - let id = Namegen.id_of_name_using_hdchar env typ name in + let id = Namegen.id_of_name_using_hdchar env sigma typ name in Namegen.next_ident_away_in_goal id (Termops.ids_of_named_context (Environ.named_context env)) | Names.Name id -> id in + let sigma = Sigma.Unsafe.of_evar_map sigma in let Sigma (evar, sigma, p) = Evarutil.new_evar env sigma ~src ~naming:(Misctypes.IntroFresh id) typ in let tac = (Tactics.letin_tac None (Names.Name id) evar None Locusops.nowhere) diff --git a/ltac/extratactics.ml4 b/ltac/extratactics.ml4 index 34159d945..58c5823c5 100644 --- a/ltac/extratactics.ml4 +++ b/ltac/extratactics.ml4 @@ -645,8 +645,6 @@ let subst_hole_with_term occ tc t = open Tacmach let hResolve id c occ t = - let c = EConstr.Unsafe.to_constr c in - let t = EConstr.Unsafe.to_constr t in Proofview.Goal.nf_s_enter { s_enter = begin fun gl -> let sigma = Proofview.Goal.sigma gl in let sigma = Sigma.to_evar_map sigma in diff --git a/plugins/decl_mode/decl_interp.ml b/plugins/decl_mode/decl_interp.ml index ae057b458..828d634d0 100644 --- a/plugins/decl_mode/decl_interp.ml +++ b/plugins/decl_mode/decl_interp.ml @@ -316,7 +316,7 @@ let rec match_aliases names constr = function let args,bnames,body = match_aliases qnames body q in st::args,bnames,body -let detype_ground env c = Detyping.detype false [] env Evd.empty c +let detype_ground env c = Detyping.detype false [] env Evd.empty (EConstr.of_constr c) let interp_cases info env sigma params (pat:cases_pattern_expr) hyps = let et,pinfo = diff --git a/plugins/decl_mode/decl_proof_instr.ml b/plugins/decl_mode/decl_proof_instr.ml index adc4ad8a3..4fe59d755 100644 --- a/plugins/decl_mode/decl_proof_instr.ml +++ b/plugins/decl_mode/decl_proof_instr.ml @@ -440,7 +440,7 @@ let concl_refiner metas body gls = [] -> anomaly ~label:"concl_refiner" (Pp.str "cannot happen") | (n,typ)::rest -> let _A = subst_meta subst typ in - let x = id_of_name_using_hdchar env _A Anonymous in + let x = id_of_name_using_hdchar env evd (EConstr.of_constr _A) Anonymous in let _x = fresh_id avoid x gls in let nenv = Environ.push_named (LocalAssum (_x,_A)) env in let asort = family_of_sort (Typing.e_sort_of nenv (ref evd) (EConstr.of_constr _A)) in @@ -895,7 +895,6 @@ let build_per_info etype casee gls = let ctyp=pf_unsafe_type_of gls (EConstr.of_constr casee) in let is_dep = dependent (project gls) (EConstr.of_constr casee) concl in let hd,args = decompose_app (special_whd gls ctyp) in - let ctyp = EConstr.Unsafe.to_constr ctyp in let (ind,u) = try destInd hd @@ -909,10 +908,11 @@ let build_per_info etype casee gls = let params,real_args = List.chop nparams args in let abstract_obj c body = let typ=pf_unsafe_type_of gls (EConstr.of_constr c) in - let typ = EConstr.Unsafe.to_constr typ in - lambda_create env (typ,subst_term (project gls) (EConstr.of_constr c) (EConstr.of_constr body)) in + lambda_create env (project gls) (typ,Termops.subst_term (project gls) (EConstr.of_constr c) body) in let pred= List.fold_right abstract_obj - real_args (lambda_create env (ctyp,subst_term (project gls) (EConstr.of_constr casee) concl)) in + real_args (lambda_create env (project gls) (ctyp,Termops.subst_term (project gls) (EConstr.of_constr casee) concl)) in + let ctyp = EConstr.Unsafe.to_constr ctyp in + let pred = EConstr.Unsafe.to_constr pred in is_dep, {per_casee=casee; per_ctype=ctyp; @@ -1275,16 +1275,15 @@ let rec execute_cases fix_name per_info tacnext args objs nhrec tree gls = let env=pf_env gls in let ctyp=pf_unsafe_type_of gls (EConstr.of_constr casee) in let hd,all_args = decompose_app (special_whd gls ctyp) in - let ctyp = EConstr.Unsafe.to_constr ctyp in let ind', u = destInd hd in let _ = assert (eq_ind ind' ind) in (* just in case *) let params,real_args = List.chop nparams all_args in let abstract_obj c body = let typ=pf_unsafe_type_of gls (EConstr.of_constr c) in - let typ = EConstr.Unsafe.to_constr typ in - lambda_create env (typ,subst_term (project gls) (EConstr.of_constr c) (EConstr.of_constr body)) in + lambda_create env (project gls) (typ,Termops.subst_term (project gls) (EConstr.of_constr c) body) in let elim_pred = List.fold_right abstract_obj - real_args (lambda_create env (ctyp,subst_term (project gls) (EConstr.of_constr casee) concl)) in + real_args (lambda_create env (project gls) (ctyp,Termops.subst_term (project gls) (EConstr.of_constr casee) concl)) in + let elim_pred = EConstr.Unsafe.to_constr elim_pred in let case_info = Inductiveops.make_case_info env ind RegularStyle in let gen_arities = Inductive.arities_of_constructors (ind,u) spec in let f_ids typ = @@ -1345,6 +1344,7 @@ let rec execute_cases fix_name per_info tacnext args objs nhrec tree gls = let understand_my_constr env sigma c concl = let env = env in + let c = EConstr.of_constr c in let rawc = Detyping.detype false [] env Evd.empty c in let rec frob = function | GEvar _ -> GHole (Loc.ghost,Evar_kinds.QuestionMark Evar_kinds.Expand,Misctypes.IntroAnonymous,None) diff --git a/plugins/funind/glob_term_to_relation.ml b/plugins/funind/glob_term_to_relation.ml index fd2f4bbd3..63bd3848f 100644 --- a/plugins/funind/glob_term_to_relation.ml +++ b/plugins/funind/glob_term_to_relation.ml @@ -421,7 +421,7 @@ let rec pattern_to_term_and_type env typ = function Array.to_list (Array.init (cst_narg - List.length patternl) - (fun i -> Detyping.detype false [] env (Evd.from_env env) csta.(i)) + (fun i -> Detyping.detype false [] env (Evd.from_env env) (EConstr.of_constr csta.(i))) ) in let patl_as_term = @@ -504,7 +504,6 @@ let rec build_entry_lc env funnames avoid rt : glob_constr build_entry_return = *) let rt_as_constr,ctx = Pretyping.understand env (Evd.from_env env) rt in let rt_typ = Typing.unsafe_type_of env (Evd.from_env env) (EConstr.of_constr rt_as_constr) in - let rt_typ = EConstr.Unsafe.to_constr rt_typ in let res_raw_type = Detyping.detype false [] env (Evd.from_env env) rt_typ in let res = fresh_id args_res.to_avoid "_res" in let new_avoid = res::args_res.to_avoid in @@ -757,7 +756,6 @@ and build_entry_lc_from_case_term env types funname make_discr patterns_to_preve let typ_of_id = Typing.unsafe_type_of env_with_pat_ids (Evd.from_env env) (EConstr.mkVar id) in - let typ_of_id = EConstr.Unsafe.to_constr typ_of_id in let raw_typ_of_id = Detyping.detype false [] env_with_pat_ids (Evd.from_env env) typ_of_id @@ -804,6 +802,7 @@ and build_entry_lc_from_case_term env types funname make_discr patterns_to_preve List.map3 (fun pat e typ_as_constr -> let this_pat_ids = ids_of_pat pat in + let typ_as_constr = EConstr.of_constr typ_as_constr in let typ = Detyping.detype false [] new_env (Evd.from_env env) typ_as_constr in let pat_as_term = pattern_to_term pat in List.fold_right @@ -811,7 +810,6 @@ and build_entry_lc_from_case_term env types funname make_discr patterns_to_preve if Id.Set.mem id this_pat_ids then (Prod (Name id), let typ_of_id = Typing.unsafe_type_of new_env (Evd.from_env env) (EConstr.mkVar id) in - let typ_of_id = EConstr.Unsafe.to_constr typ_of_id in let raw_typ_of_id = Detyping.detype false [] new_env (Evd.from_env env) typ_of_id in @@ -970,7 +968,7 @@ let rec rebuild_cons env nb_args relname args crossed_types depth rt = (List.map (fun p -> Detyping.detype false [] env (Evd.from_env env) - p) params)@(Array.to_list + (EConstr.of_constr p)) params)@(Array.to_list (Array.make (List.length args' - nparam) (mkGHole ())))) @@ -988,6 +986,7 @@ let rec rebuild_cons env nb_args relname args crossed_types depth rt = let ty' = snd (Util.List.chop nparam ty) in List.fold_left2 (fun acc var_as_constr arg -> + let arg = EConstr.of_constr arg in if isRel var_as_constr then let na = RelDecl.get_name (Environ.lookup_rel (destRel var_as_constr) env) in diff --git a/plugins/funind/merge.ml b/plugins/funind/merge.ml index 691385fad..44aacaf45 100644 --- a/plugins/funind/merge.ml +++ b/plugins/funind/merge.ml @@ -777,6 +777,7 @@ let merge_inductive_body (shift:merge_infos) avoid (oib1:one_inductive_body) let mkrawcor nme avoid typ = (* first replace rel 1 by a varname *) let substindtyp = substitterm 0 (mkRel 1) (mkVar nme) typ in + let substindtyp = EConstr.of_constr substindtyp in Detyping.detype false (Id.Set.elements avoid) (Global.env()) Evd.empty substindtyp in let lcstr1: glob_constr list = Array.to_list (Array.map (mkrawcor ind1name avoid) oib1.mind_user_lc) in @@ -860,6 +861,7 @@ let glob_constr_list_to_inductive_expr prms1 prms2 mib1 mib2 shift let mkProd_reldecl (rdecl:Context.Rel.Declaration.t) (t2:glob_constr) = match rdecl with | LocalAssum (nme,t) -> + let t = EConstr.of_constr t in let traw = Detyping.detype false [] (Global.env()) Evd.empty t in GProd (Loc.ghost,nme,Explicit,traw,t2) | LocalDef _ -> assert false diff --git a/plugins/funind/recdef.ml b/plugins/funind/recdef.ml index f5ea32878..2a66ba852 100644 --- a/plugins/funind/recdef.ml +++ b/plugins/funind/recdef.ml @@ -122,8 +122,8 @@ let pf_get_new_ids idl g = [] let compute_renamed_type gls c = - EConstr.of_constr (rename_bound_vars_as_displayed (*no avoid*) [] (*no rels*) [] - (EConstr.Unsafe.to_constr (pf_unsafe_type_of gls c))) + rename_bound_vars_as_displayed (project gls) (*no avoid*) [] (*no rels*) [] + (pf_unsafe_type_of gls c) let h'_id = Id.of_string "h'" let teq_id = Id.of_string "teq" let ano_id = Id.of_string "anonymous" diff --git a/pretyping/cases.ml b/pretyping/cases.ml index a5a5fe6d2..490bc2801 100644 --- a/pretyping/cases.ml +++ b/pretyping/cases.ml @@ -708,7 +708,7 @@ let merge_name get_name obj = function let merge_names get_name = List.map2 (merge_name get_name) -let get_names env sign eqns = +let get_names env sigma sign eqns = let names1 = List.make (Context.Rel.length sign) Anonymous in (* If any, we prefer names used in pats, from top to bottom *) let names2,aliasname = @@ -727,7 +727,7 @@ let get_names env sign eqns = (fun (l,avoid) d na -> let na = merge_name - (fun (LocalAssum (na,t) | LocalDef (na,_,t)) -> Name (next_name_away (named_hd env (EConstr.Unsafe.to_constr t) na) avoid)) + (fun (LocalAssum (na,t) | LocalDef (na,_,t)) -> Name (next_name_away (named_hd env sigma t na) avoid)) d na in (na::l,(out_name na)::avoid)) @@ -924,7 +924,7 @@ let rec extract_predicate ccl = function ccl let abstract_predicate env sigma indf cur realargs (names,na) tms ccl = - let sign = make_arity_signature env true indf in + let sign = make_arity_signature env sigma true indf in (* n is the number of real args + 1 (+ possible let-ins in sign) *) let n = List.length sign in (* Before abstracting we generalize over cur and on those realargs *) @@ -945,7 +945,7 @@ let abstract_predicate env sigma indf cur realargs (names,na) tms ccl = let pred = extract_predicate ccl tms in (* Build the predicate properly speaking *) let sign = List.map2 set_name (na::names) sign in - EConstr.of_constr (it_mkLambda_or_LetIn_name env (EConstr.Unsafe.to_constr pred) sign) + it_mkLambda_or_LetIn_name env sigma pred sign (* [expand_arg] is used by [specialize_predicate] if Yk denotes [Xk;xk] or [Xk], @@ -1238,7 +1238,7 @@ let build_branch initial current realargs deps (realnames,curname) pb arsign eqn (* that had matched constructor C *) let cs_args = const_info.cs_args in let cs_args = List.map (fun d -> map_rel_decl EConstr.of_constr d) cs_args in - let names,aliasname = get_names pb.env cs_args eqns in + let names,aliasname = get_names pb.env !(pb.evdref) cs_args eqns in let typs = List.map2 RelDecl.set_name names cs_args in @@ -1714,7 +1714,7 @@ let build_tycon loc env tycon_env s subst tycon extenv evdref t = let build_inversion_problem loc env sigma tms t = let make_patvar t (subst,avoid) = - let id = next_name_away (named_hd env (EConstr.Unsafe.to_constr t) Anonymous) avoid in + let id = next_name_away (named_hd env sigma t Anonymous) avoid in PatVar (Loc.ghost,Name id), ((id,t)::subst, id::avoid) in let rec reveal_pattern t (subst,avoid as acc) = match EConstr.kind sigma (whd_all env sigma t) with @@ -1733,8 +1733,7 @@ let build_inversion_problem loc env sigma tms t = let patl,acc = List.fold_map' reveal_pattern realargs acc in let pat,acc = make_patvar t acc in let indf' = lift_inductive_family n indf in - let sign = make_arity_signature env true indf' in - let sign = List.map (fun d -> map_rel_decl EConstr.of_constr d) sign in + let sign = make_arity_signature env sigma true indf' in let patl = pat :: List.rev patl in let patl,sign = recover_and_adjust_alias_names patl sign in let p = List.length patl in diff --git a/pretyping/detyping.ml b/pretyping/detyping.ml index c8d945c0b..1adda14ab 100644 --- a/pretyping/detyping.ml +++ b/pretyping/detyping.ml @@ -6,14 +6,17 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) +module CVars = Vars + open Pp open CErrors open Util open Names open Term +open Environ +open EConstr open Vars open Inductiveops -open Environ open Glob_term open Glob_ops open Termops @@ -188,7 +191,7 @@ let _ = declare_bool_option (* Auxiliary function for MutCase printing *) (* [computable] tries to tell if the predicate typing the result is inferable*) -let computable p k = +let computable sigma p k = (* We first remove as many lambda as the arity, then we look if it remains a lambda for a dependent elimination. This function works for normal eta-expanded term. For non eta-expanded or @@ -205,31 +208,29 @@ let computable p k = sinon on perd la réciprocité de la synthèse (qui, lui, engendrera un prédicat non dépendant) *) - let sign,ccl = decompose_lam_assum p in + let sign,ccl = decompose_lam_assum sigma p in Int.equal (Context.Rel.length sign) (k + 1) && - noccur_between 1 (k+1) ccl + noccur_between sigma 1 (k+1) ccl -let pop t = Vars.lift (-1) t - -let lookup_name_as_displayed env t s = - let rec lookup avoid n c = match kind_of_term c with +let lookup_name_as_displayed env sigma t s = + let rec lookup avoid n c = match EConstr.kind sigma c with | Prod (name,_,c') -> - (match compute_displayed_name_in RenamingForGoal avoid name c' with + (match compute_displayed_name_in sigma RenamingForGoal avoid name c' with | (Name id,avoid') -> if Id.equal id s then Some n else lookup avoid' (n+1) c' | (Anonymous,avoid') -> lookup avoid' (n+1) (pop c')) | LetIn (name,_,_,c') -> - (match compute_displayed_name_in RenamingForGoal avoid name c' with + (match compute_displayed_name_in sigma RenamingForGoal avoid name c' with | (Name id,avoid') -> if Id.equal id s then Some n else lookup avoid' (n+1) c' | (Anonymous,avoid') -> lookup avoid' (n+1) (pop c')) | Cast (c,_,_) -> lookup avoid n c | _ -> None in lookup (ids_of_named_context (named_context env)) 1 t -let lookup_index_as_renamed env t n = - let rec lookup n d c = match kind_of_term c with +let lookup_index_as_renamed env sigma t n = + let rec lookup n d c = match EConstr.kind sigma c with | Prod (name,_,c') -> - (match compute_displayed_name_in RenamingForGoal [] name c' with + (match compute_displayed_name_in sigma RenamingForGoal [] name c' with (Name _,_) -> lookup n (d+1) c' | (Anonymous,_) -> if Int.equal n 0 then @@ -239,7 +240,7 @@ let lookup_index_as_renamed env t n = else lookup (n-1) (d+1) c') | LetIn (name,_,_,c') -> - (match compute_displayed_name_in RenamingForGoal [] name c' with + (match compute_displayed_name_in sigma RenamingForGoal [] name c' with | (Name _,_) -> lookup n (d+1) c' | (Anonymous,_) -> if Int.equal n 0 then @@ -256,9 +257,9 @@ let lookup_index_as_renamed env t n = (**********************************************************************) (* Fragile algorithm to reverse pattern-matching compilation *) -let update_name na ((_,(e,_)),c) = +let update_name sigma na ((_,(e,_)),c) = match na with - | Name _ when force_wildcard () && noccurn (List.index Name.equal na e) c -> + | Name _ when force_wildcard () && noccurn sigma (List.index Name.equal na e) c -> Anonymous | _ -> na @@ -269,7 +270,7 @@ let rec decomp_branch tags nal b (avoid,env as e) sigma c = | [] -> (List.rev nal,(e,c)) | b::tags -> let na,c,f,body,t = - match kind_of_term (EConstr.Unsafe.to_constr (strip_outer_cast sigma (EConstr.of_constr c))), b with + match EConstr.kind sigma (strip_outer_cast sigma c), b with | Lambda (na,t,c),false -> na,c,compute_displayed_let_name_in,None,Some t | LetIn (na,b,t,c),true -> na,c,compute_displayed_name_in,Some b,Some t @@ -279,12 +280,12 @@ let rec decomp_branch tags nal b (avoid,env as e) sigma c = | _, true -> Anonymous,lift 1 c,compute_displayed_name_in,None,None in - let na',avoid' = f flag avoid na c in + let na',avoid' = f sigma flag avoid na c in decomp_branch tags (na'::nal) b (avoid', add_name_opt na' body t env) sigma c let rec build_tree na isgoal e sigma ci cl = - let mkpat n rhs pl = PatCstr(dl,(ci.ci_ind,n+1),pl,update_name na rhs) in + let mkpat n rhs pl = PatCstr(dl,(ci.ci_ind,n+1),pl,update_name sigma na rhs) in let cnl = ci.ci_pp_info.cstr_tags in let cna = ci.ci_cstr_nargs in List.flatten @@ -294,12 +295,12 @@ let rec build_tree na isgoal e sigma ci cl = and align_tree nal isgoal (e,c as rhs) sigma = match nal with | [] -> [[],rhs] | na::nal -> - match kind_of_term c with + match EConstr.kind sigma c with | Case (ci,p,c,cl) when - eq_constr sigma (EConstr.of_constr c) (EConstr.mkRel (List.index Name.equal na (fst (snd e)))) + eq_constr sigma c (mkRel (List.index Name.equal na (fst (snd e)))) && not (Int.equal (Array.length cl) 0) && (* don't contract if p dependent *) - computable p (List.length ci.ci_pp_info.ind_tags) (* FIXME: can do better *) -> + computable sigma p (List.length ci.ci_pp_info.ind_tags) (* FIXME: can do better *) -> let clauses = build_tree na isgoal e sigma ci cl in List.flatten (List.map (fun (pat,rhs) -> @@ -307,7 +308,7 @@ and align_tree nal isgoal (e,c as rhs) sigma = match nal with List.map (fun (hd,rest) -> pat::hd,rest) lines) clauses) | _ -> - let pat = PatVar(dl,update_name na rhs) in + let pat = PatVar(dl,update_name sigma na rhs) in let mat = align_tree nal isgoal rhs sigma in List.map (fun (hd,rest) -> pat::hd,rest) mat @@ -320,11 +321,11 @@ and contract_branch isgoal e sigma (cdn,can,mkpat,b) = (* Transform internal representation of pattern-matching into list of *) (* clauses *) -let is_nondep_branch c l = +let is_nondep_branch sigma c l = try (* FIXME: do better using tags from l *) - let sign,ccl = decompose_lam_n_decls (List.length l) c in - noccur_between 1 (Context.Rel.length sign) ccl + let sign,ccl = decompose_lam_n_decls sigma (List.length l) c in + noccur_between sigma 1 (Context.Rel.length sign) ccl with e when CErrors.noncritical e -> (* Not eta-expanded or not reduced *) false @@ -441,7 +442,7 @@ let detype_instance sigma l = else Some (List.map (detype_level sigma) (Array.to_list (Univ.Instance.to_array l))) let rec detype flags avoid env sigma t = - match kind_of_term (EConstr.Unsafe.to_constr (collapse_appl sigma (EConstr.of_constr t))) with + match EConstr.kind sigma (collapse_appl sigma t) with | Rel n -> (try match lookup_name_of_rel n (fst env) with | Name id -> GVar (dl, id) @@ -503,11 +504,11 @@ let rec detype flags avoid env sigma t = try let pb = Environ.lookup_projection p (snd env) in let body = pb.Declarations.proj_body in - let ty = Retyping.get_type_of (snd env) sigma (EConstr.of_constr c) in + let ty = Retyping.get_type_of (snd env) sigma c in let ((ind,u), args) = Inductiveops.find_mrectype (snd env) sigma ty in - let args = List.map EConstr.Unsafe.to_constr args in let body' = strip_lam_assum body in - let body' = subst_instance_constr u body' in + let body' = CVars.subst_instance_constr u body' in + let body' = EConstr.of_constr body' in substl (c :: List.rev args) body' with Retyping.RetypeError _ | Not_found -> anomaly (str"Cannot detype an unfolded primitive projection.") @@ -515,8 +516,7 @@ let rec detype flags avoid env sigma t = else if print_primproj_params () then try - let c = Retyping.expand_projection (snd env) sigma p (EConstr.of_constr c) [] in - let c = EConstr.Unsafe.to_constr c in + let c = Retyping.expand_projection (snd env) sigma p c [] in detype flags avoid env sigma c with Retyping.RetypeError _ -> noparams () else noparams () @@ -527,8 +527,8 @@ let rec detype flags avoid env sigma t = | LocalDef _ -> true | LocalAssum (id,_) -> try let n = List.index Name.equal (Name id) (fst env) in - isRelN n c - with Not_found -> isVarId id c + isRelN sigma n c + with Not_found -> isVarId sigma id c in let id,l = try @@ -537,8 +537,8 @@ let rec detype flags avoid env sigma t = | Some id -> id in let l = Evd.evar_instance_array bound_to_itself_or_letin (Evd.find sigma evk) cl in - let fvs,rels = List.fold_left (fun (fvs,rels) (_,c) -> match kind_of_term c with Rel n -> (fvs,Int.Set.add n rels) | Var id -> (Id.Set.add id fvs,rels) | _ -> (fvs,rels)) (Id.Set.empty,Int.Set.empty) l in - let l = Evd.evar_instance_array (fun d c -> not !print_evar_arguments && (bound_to_itself_or_letin d c && not (isRel c && Int.Set.mem (destRel c) rels || isVar c && (Id.Set.mem (destVar c) fvs)))) (Evd.find sigma evk) cl in + let fvs,rels = List.fold_left (fun (fvs,rels) (_,c) -> match EConstr.kind sigma c with Rel n -> (fvs,Int.Set.add n rels) | Var id -> (Id.Set.add id fvs,rels) | _ -> (fvs,rels)) (Id.Set.empty,Int.Set.empty) l in + let l = Evd.evar_instance_array (fun d c -> not !print_evar_arguments && (bound_to_itself_or_letin d c && not (isRel sigma c && Int.Set.mem (destRel sigma c) rels || isVar sigma c && (Id.Set.mem (destVar sigma c) fvs)))) (Evd.find sigma evk) cl in id,l with Not_found -> Id.of_string ("X" ^ string_of_int (Evar.repr evk)), @@ -551,10 +551,10 @@ let rec detype flags avoid env sigma t = | Construct (cstr_sp,u) -> GRef (dl, ConstructRef cstr_sp, detype_instance sigma u) | Case (ci,p,c,bl) -> - let comp = computable p (List.length (ci.ci_pp_info.ind_tags)) in + let comp = computable sigma p (List.length (ci.ci_pp_info.ind_tags)) in detype_case comp (detype flags avoid env sigma) (detype_eqns flags avoid env sigma ci comp) - is_nondep_branch avoid + (is_nondep_branch sigma) avoid (ci.ci_ind,ci.ci_pp_info.style, ci.ci_pp_info.cstr_tags,ci.ci_pp_info.ind_tags) (Some p) c bl @@ -594,7 +594,7 @@ and detype_cofix flags avoid env sigma n (names,tys,bodies) = Array.map (fun (_,bd,_) -> bd) v) and share_names flags n l avoid env sigma c t = - match kind_of_term c, kind_of_term t with + match EConstr.kind sigma c, EConstr.kind sigma t with (* factorize even when not necessary to have better presentation *) | Lambda (na,t,c), Prod (na',t',c') -> let na = match (na,na') with @@ -641,15 +641,15 @@ and detype_eqns flags avoid env sigma ci computable constructs consnargsl bl = and detype_eqn (lax,isgoal as flags) avoid env sigma constr construct_nargs branch = let make_pat x avoid env b body ty ids = - if force_wildcard () && noccurn 1 b then + if force_wildcard () && noccurn sigma 1 b then PatVar (dl,Anonymous),avoid,(add_name Anonymous body ty env),ids else let flag = if isgoal then RenamingForGoal else RenamingForCasesPattern (fst env,b) in - let na,avoid' = compute_displayed_name_in flag avoid x b in + let na,avoid' = compute_displayed_name_in sigma flag avoid x b in PatVar (dl,na),avoid',(add_name na body ty env),add_vname ids na in let rec buildrec ids patlist avoid env l b = - match kind_of_term b, l with + match EConstr.kind sigma b, l with | _, [] -> (dl, Id.Set.elements ids, [PatCstr(dl, constr, List.rev patlist,Anonymous)], @@ -684,8 +684,8 @@ and detype_eqn (lax,isgoal as flags) avoid env sigma constr construct_nargs bran and detype_binder (lax,isgoal as flags) bk avoid env sigma na body ty c = let flag = if isgoal then RenamingForGoal else RenamingElsewhereFor (fst env,c) in let na',avoid' = match bk with - | BLetIn -> compute_displayed_let_name_in flag avoid na c - | _ -> compute_displayed_name_in flag avoid na c in + | BLetIn -> compute_displayed_let_name_in sigma flag avoid na c + | _ -> compute_displayed_name_in sigma flag avoid na c in let r = detype flags avoid' (add_name na' body ty env) sigma c in match bk with | BProd -> GProd (dl, na',Explicit,detype (lax,false) avoid env sigma ty, r) @@ -693,13 +693,13 @@ and detype_binder (lax,isgoal as flags) bk avoid env sigma na body ty c = | BLetIn -> let c = detype (lax,false) avoid env sigma (Option.get body) in (* Heuristic: we display the type if in Prop *) - let s = try Retyping.get_sort_family_of (snd env) sigma (EConstr.of_constr ty) with _ when !Flags.in_debugger || !Flags.in_toplevel -> InType (* Can fail because of sigma missing in debugger *) in + let s = try Retyping.get_sort_family_of (snd env) sigma ty with _ when !Flags.in_debugger || !Flags.in_toplevel -> InType (* Can fail because of sigma missing in debugger *) in let c = if s != InProp then c else GCast (dl, c, CastConv (detype (lax,false) avoid env sigma ty)) in GLetIn (dl, na', c, r) let detype_rel_context ?(lax=false) where avoid env sigma sign = - let where = Option.map (fun c -> it_mkLambda_or_LetIn c sign) where in + let where = Option.map (fun c -> EConstr.it_mkLambda_or_LetIn c sign) where in let rec aux avoid env = function | [] -> [] | decl::rest -> @@ -711,10 +711,10 @@ let detype_rel_context ?(lax=false) where avoid env sigma sign = | None -> na,avoid | Some c -> if is_local_def decl then - compute_displayed_let_name_in + compute_displayed_let_name_in sigma (RenamingElsewhereFor (fst env,c)) avoid na c else - compute_displayed_name_in + compute_displayed_name_in sigma (RenamingElsewhereFor (fst env,c)) avoid na c in let b = match decl with | LocalAssum _ -> None @@ -731,6 +731,7 @@ let detype ?(lax=false) isgoal avoid env sigma t = detype (lax,isgoal) avoid (names_of_rel_context env, env) sigma t let detype_closed_glob ?lax isgoal avoid env sigma t = + let open Context.Rel.Declaration in let convert_id cl id = try Id.Map.find id cl.idents with Not_found -> id @@ -748,12 +749,11 @@ let detype_closed_glob ?lax isgoal avoid env sigma t = with Not_found -> try (* assumes [detype] does not raise [Not_found] exceptions *) let (b,c) = Id.Map.find id cl.typed in - let c = EConstr.Unsafe.to_constr c in (* spiwack: I'm not sure it is the right thing to do, but I'm computing the detyping environment like [Printer.pr_constr_under_binders_env] does. *) - let assums = List.map (fun id -> (Name id,(* dummy *) mkProp)) b in - let env = Termops.push_rels_assum assums env in + let assums = List.map (fun id -> LocalAssum (Name id,(* dummy *) mkProp)) b in + let env = push_rel_context assums env in detype ?lax isgoal avoid env sigma c (* if [id] is bound to a [closed_glob_constr]. *) with Not_found -> try @@ -808,7 +808,7 @@ let rec subst_glob_constr subst raw = | GRef (loc,ref,u) -> let ref',t = subst_global subst ref in if ref' == ref then raw else - detype false [] (Global.env()) Evd.empty t + detype false [] (Global.env()) Evd.empty (EConstr.of_constr t) | GVar _ -> raw | GEvar _ -> raw diff --git a/pretyping/detyping.mli b/pretyping/detyping.mli index c51cb0f44..4c6f9129f 100644 --- a/pretyping/detyping.mli +++ b/pretyping/detyping.mli @@ -9,6 +9,7 @@ open Names open Term open Environ +open EConstr open Glob_term open Termops open Mod_subst @@ -45,13 +46,13 @@ val detype_case : val detype_sort : evar_map -> sorts -> glob_sort val detype_rel_context : ?lax:bool -> constr option -> Id.t list -> (names_context * env) -> - evar_map -> Context.Rel.t -> glob_decl list + evar_map -> rel_context -> glob_decl list val detype_closed_glob : ?lax:bool -> bool -> Id.t list -> env -> evar_map -> closed_glob_constr -> glob_constr (** look for the index of a named var or a nondep var as it is renamed *) -val lookup_name_as_displayed : env -> constr -> Id.t -> int option -val lookup_index_as_renamed : env -> constr -> int -> int option +val lookup_name_as_displayed : env -> evar_map -> constr -> Id.t -> int option +val lookup_index_as_renamed : env -> evar_map -> constr -> int -> int option val set_detype_anonymous : (Loc.t -> int -> glob_constr) -> unit val force_wildcard : unit -> bool diff --git a/pretyping/evardefine.ml b/pretyping/evardefine.ml index faf34baf7..20d86f81b 100644 --- a/pretyping/evardefine.ml +++ b/pretyping/evardefine.ml @@ -140,7 +140,7 @@ let define_pure_evar_as_lambda env evd evk = | _ -> error_not_product env evd typ in let avoid = ids_of_named_context (evar_context evi) in let id = - next_name_away_with_default_using_types "x" na avoid (EConstr.Unsafe.to_constr (Reductionops.whd_evar evd dom)) in + next_name_away_with_default_using_types "x" na avoid (Reductionops.whd_evar evd dom) in let newenv = push_named (LocalAssum (id, dom)) evenv in let filter = Filter.extend 1 (evar_filter evi) in let src = evar_source evk evd1 in diff --git a/pretyping/indrec.ml b/pretyping/indrec.ml index 431d1ff16..c4a74d990 100644 --- a/pretyping/indrec.ml +++ b/pretyping/indrec.ml @@ -40,6 +40,18 @@ type recursion_scheme_error = exception RecursionSchemeError of recursion_scheme_error +let named_hd env t na = named_hd env Evd.empty (EConstr.of_constr t) na +let name_assumption env = function +| LocalAssum (na,t) -> LocalAssum (named_hd env t na, t) +| LocalDef (na,c,t) -> LocalDef (named_hd env c na, c, t) + +let mkLambda_or_LetIn_name env d b = mkLambda_or_LetIn (name_assumption env d) b +let mkProd_or_LetIn_name env d b = mkProd_or_LetIn (name_assumption env d) b +let mkLambda_name env (n,a,b) = mkLambda_or_LetIn_name env (LocalAssum (n,a)) b +let mkProd_name env (n,a,b) = mkProd_or_LetIn_name env (LocalAssum (n,a)) b +let it_mkProd_or_LetIn_name env b l = List.fold_left (fun c d -> mkProd_or_LetIn_name env d c) b l +let it_mkLambda_or_LetIn_name env b l = List.fold_left (fun c d -> mkLambda_or_LetIn_name env d c) b l + let make_prod_dep dep env = if dep then mkProd_name env else mkProd let mkLambda_string s t c = mkLambda (Name (Id.of_string s), t, c) @@ -118,12 +130,13 @@ let mis_make_case_com dep env sigma (ind, u as pind) (mib,mip as specif) kind = it_mkLambda_or_LetIn_name env' obj deparsign else let cs = lift_constructor (k+1) constrs.(k) in - let t = build_branch_type env dep (mkRel (k+1)) cs in + let t = build_branch_type env (Sigma.to_evar_map sigma) dep (mkRel (k+1)) cs in mkLambda_string "f" t (add_branch (push_rel (LocalAssum (Anonymous, t)) env) (k+1)) in let Sigma (s, sigma, p) = Sigma.fresh_sort_in_family ~rigid:Evd.univ_flexible_alg env sigma kind in - let typP = make_arity env' dep indf s in + let typP = make_arity env' (Sigma.to_evar_map sigma) dep indf s in + let typP = EConstr.Unsafe.to_constr typP in let c = it_mkLambda_or_LetIn_name env (mkLambda_string "P" typP @@ -443,7 +456,8 @@ let mis_make_indrec env sigma listdepkind mib u = Evarutil.evd_comb1 (Evd.fresh_sort_in_family ~rigid:Evd.univ_flexible_alg env) evdref kinds in - let typP = make_arity env dep indf s in + let typP = make_arity env !evdref dep indf s in + let typP = EConstr.Unsafe.to_constr typP in mkLambda_string "P" typP (put_arity (push_rel (LocalAssum (Anonymous,typP)) env) (i+1) rest) | [] -> diff --git a/pretyping/inductiveops.ml b/pretyping/inductiveops.ml index 3191a58ff..9e823ab4c 100644 --- a/pretyping/inductiveops.ml +++ b/pretyping/inductiveops.ml @@ -422,26 +422,29 @@ let build_dependent_inductive env ((ind, params) as indf) = (* builds the arity of an elimination predicate in sort [s] *) -let make_arity_signature env dep indf = +let make_arity_signature env sigma dep indf = let (arsign,_) = get_arity env indf in + let arsign = List.map (fun d -> Termops.map_rel_decl EConstr.of_constr d) arsign in if dep then (* We need names everywhere *) - Namegen.name_context env - ((LocalAssum (Anonymous,build_dependent_inductive env indf))::arsign) + Namegen.name_context env sigma + ((LocalAssum (Anonymous,EConstr.of_constr (build_dependent_inductive env indf)))::arsign) (* Costly: would be better to name once for all at definition time *) else (* No need to enforce names *) arsign -let make_arity env dep indf s = mkArity (make_arity_signature env dep indf, s) +let make_arity env sigma dep indf s = + let open EConstr in + it_mkProd_or_LetIn (mkSort s) (make_arity_signature env sigma dep indf) (* [p] is the predicate and [cs] a constructor summary *) -let build_branch_type env dep p cs = +let build_branch_type env sigma dep p cs = let base = appvect (lift cs.cs_nargs p, cs.cs_concl_realargs) in if dep then - Namegen.it_mkProd_or_LetIn_name env - (applist (base,[build_dependent_constructor cs])) - cs.cs_args + EConstr.Unsafe.to_constr (Namegen.it_mkProd_or_LetIn_name env sigma + (EConstr.of_constr (applist (base,[build_dependent_constructor cs]))) + (List.map (fun d -> Termops.map_rel_decl EConstr.of_constr d) cs.cs_args)) else Term.it_mkProd_or_LetIn base cs.cs_args @@ -542,11 +545,12 @@ let is_elim_predicate_explicitly_dependent env sigma pred indf = let arsign,_ = get_arity env indf in is_predicate_explicitly_dep env sigma pred arsign -let set_names env n brty = - let (ctxt,cl) = decompose_prod_n_assum n brty in - Namegen.it_mkProd_or_LetIn_name env cl ctxt +let set_names env sigma n brty = + let open EConstr in + let (ctxt,cl) = decompose_prod_n_assum sigma n brty in + EConstr.Unsafe.to_constr (Namegen.it_mkProd_or_LetIn_name env sigma cl ctxt) -let set_pattern_names env ind brv = +let set_pattern_names env sigma ind brv = let (mib,mip) = Inductive.lookup_mind_specif env ind in let arities = Array.map @@ -554,7 +558,7 @@ let set_pattern_names env ind brv = Context.Rel.length ((prod_assum c)) - mib.mind_nparams) mip.mind_nf_lc in - Array.map2 (set_names env) arities brv + Array.map2 (set_names env sigma) arities brv let type_case_branches_with_names env sigma indspec p c = let (ind,args) = indspec in @@ -567,7 +571,7 @@ let type_case_branches_with_names env sigma indspec p c = let conclty = lambda_appvect_assum (mip.mind_nrealdecls+1) p (Array.of_list (realargs@[c])) in (* Adjust names *) if is_elim_predicate_explicitly_dependent env sigma p (ind,params) then - (set_pattern_names env (fst ind) lbrty, conclty) + (set_pattern_names env sigma (fst ind) (Array.map EConstr.of_constr lbrty), conclty) else (lbrty, conclty) (* Type of Case predicates *) diff --git a/pretyping/inductiveops.mli b/pretyping/inductiveops.mli index 4bb484759..ab470a540 100644 --- a/pretyping/inductiveops.mli +++ b/pretyping/inductiveops.mli @@ -156,9 +156,9 @@ val get_arity : env -> inductive_family -> Context.Rel.t * sorts_family val build_dependent_constructor : constructor_summary -> constr val build_dependent_inductive : env -> inductive_family -> constr -val make_arity_signature : env -> bool -> inductive_family -> Context.Rel.t -val make_arity : env -> bool -> inductive_family -> sorts -> types -val build_branch_type : env -> bool -> constr -> constructor_summary -> types +val make_arity_signature : env -> evar_map -> bool -> inductive_family -> EConstr.rel_context +val make_arity : env -> evar_map -> bool -> inductive_family -> sorts -> EConstr.types +val build_branch_type : env -> evar_map -> bool -> constr -> constructor_summary -> types (** Raise [Not_found] if not given a valid inductive type *) val extract_mrectype : evar_map -> EConstr.t -> pinductive * EConstr.constr list diff --git a/pretyping/pretyping.ml b/pretyping/pretyping.ml index 2470decdd..563769df5 100644 --- a/pretyping/pretyping.ml +++ b/pretyping/pretyping.ml @@ -79,26 +79,26 @@ type t = { (** Delay the computation of the evar extended environment *) } -let get_extra env = +let get_extra env sigma = let open Context.Named.Declaration in let ids = List.map get_id (named_context env) in let avoid = List.fold_right Id.Set.add ids Id.Set.empty in - Context.Rel.fold_outside push_rel_decl_to_named_context + Context.Rel.fold_outside (fun d acc -> push_rel_decl_to_named_context sigma d acc) (rel_context env) ~init:(empty_csubst, [], avoid, named_context env) -let make_env env = { env = env; extra = lazy (get_extra env) } +let make_env env sigma = { env = env; extra = lazy (get_extra env sigma) } let rel_context env = rel_context env.env -let push_rel d env = { +let push_rel sigma d env = { env = push_rel d env.env; - extra = lazy (push_rel_decl_to_named_context d (Lazy.force env.extra)); + extra = lazy (push_rel_decl_to_named_context sigma d (Lazy.force env.extra)); } -let pop_rel_context n env = make_env (pop_rel_context n env.env) +let pop_rel_context n env sigma = make_env (pop_rel_context n env.env) sigma -let push_rel_context ctx env = { +let push_rel_context sigma ctx env = { env = push_rel_context ctx env.env; - extra = lazy (List.fold_right push_rel_decl_to_named_context ctx (Lazy.force env.extra)); + extra = lazy (List.fold_right (fun d acc -> push_rel_decl_to_named_context sigma d acc) ctx (Lazy.force env.extra)); } let lookup_named id env = lookup_named id env.env @@ -117,9 +117,9 @@ let e_new_evar env evdref ?src ?naming typ = evdref := Sigma.to_evar_map sigma; e -let push_rec_types (lna,typarray,_) env = +let push_rec_types sigma (lna,typarray,_) env = let ctxt = Array.map2_i (fun i na t -> Context.Rel.Declaration.LocalAssum (na, lift i t)) lna typarray in - Array.fold_left (fun e assum -> push_rel assum e) env ctxt + Array.fold_left (fun e assum -> push_rel sigma assum e) env ctxt end @@ -391,7 +391,7 @@ let ltac_interp_name { ltac_idents ; ltac_genargs } = function str"It cannot be used in a binder.") else n -let ltac_interp_name_env k0 lvar env = +let ltac_interp_name_env k0 lvar env sigma = (* envhd is the initial part of the env when pretype was called first *) (* (in practice is is probably 0, but we have to grant the specification of pretype which accepts to start with a non empty @@ -402,7 +402,7 @@ let ltac_interp_name_env k0 lvar env = let open Context.Rel.Declaration in let ctxt' = List.smartmap (map_name (ltac_interp_name lvar)) ctxt in if List.equal (fun d1 d2 -> Name.equal (get_name d1) (get_name d2)) ctxt ctxt' then env - else push_rel_context ctxt' (pop_rel_context n env) + else push_rel_context sigma ctxt' (pop_rel_context n env sigma) let invert_ltac_bound_name lvar env id0 id = let id' = Id.Map.find id lvar.ltac_idents in @@ -426,7 +426,7 @@ let pretype_id pretype k0 loc env evdref lvar id = let (n,_,typ) = lookup_rel_id id (rel_context env) in { uj_val = mkRel n; uj_type = lift n typ } with Not_found -> - let env = ltac_interp_name_env k0 lvar env in + let env = ltac_interp_name_env k0 lvar env !evdref in (* Check if [id] is an ltac variable *) try let (ids,c) = Id.Map.find id lvar.ltac_constrs in @@ -569,7 +569,7 @@ let rec pretype k0 resolve_tc (tycon : type_constraint) (env : ExtraEnv.t) evdre inh_conv_coerce_to_tycon loc env evdref j tycon | GPatVar (loc,(someta,n)) -> - let env = ltac_interp_name_env k0 lvar env in + let env = ltac_interp_name_env k0 lvar env !evdref in let ty = match tycon with | Some ty -> ty @@ -578,7 +578,7 @@ let rec pretype k0 resolve_tc (tycon : type_constraint) (env : ExtraEnv.t) evdre { uj_val = e_new_evar env evdref ~src:(loc,k) ty; uj_type = ty } | GHole (loc, k, naming, None) -> - let env = ltac_interp_name_env k0 lvar env in + let env = ltac_interp_name_env k0 lvar env !evdref in let ty = match tycon with | Some ty -> ty @@ -587,7 +587,7 @@ let rec pretype k0 resolve_tc (tycon : type_constraint) (env : ExtraEnv.t) evdre { uj_val = e_new_evar env evdref ~src:(loc,k) ~naming ty; uj_type = ty } | GHole (loc, k, _naming, Some arg) -> - let env = ltac_interp_name_env k0 lvar env in + let env = ltac_interp_name_env k0 lvar env !evdref in let ty = match tycon with | Some ty -> ty @@ -605,18 +605,18 @@ let rec pretype k0 resolve_tc (tycon : type_constraint) (env : ExtraEnv.t) evdre let ty' = pretype_type empty_valcon env evdref lvar ty in let dcl = LocalAssum (na, ty'.utj_val) in let dcl' = LocalAssum (ltac_interp_name lvar na,ty'.utj_val) in - type_bl (push_rel dcl env) (Context.Rel.add dcl' ctxt) bl + type_bl (push_rel !evdref dcl env) (Context.Rel.add dcl' ctxt) bl | (na,bk,Some bd,ty)::bl -> let ty' = pretype_type empty_valcon env evdref lvar ty in let bd' = pretype (mk_tycon ty'.utj_val) env evdref lvar bd in let dcl = LocalDef (na, bd'.uj_val, ty'.utj_val) in let dcl' = LocalDef (ltac_interp_name lvar na, bd'.uj_val, ty'.utj_val) in - type_bl (push_rel dcl env) (Context.Rel.add dcl' ctxt) bl in + type_bl (push_rel !evdref dcl env) (Context.Rel.add dcl' ctxt) bl in let ctxtv = Array.map (type_bl env Context.Rel.empty) bl in let larj = Array.map2 (fun e ar -> - pretype_type empty_valcon (push_rel_context e env) evdref lvar ar) + pretype_type empty_valcon (push_rel_context !evdref e env) evdref lvar ar) ctxtv lar in let lara = Array.map (fun a -> a.utj_val) larj in let ftys = Array.map2 (fun e a -> it_mkProd_or_LetIn a e) ctxtv lara in @@ -632,7 +632,7 @@ let rec pretype k0 resolve_tc (tycon : type_constraint) (env : ExtraEnv.t) evdre | None -> true in (* Note: bodies are not used by push_rec_types, so [||] is safe *) - let newenv = push_rec_types (names,ftys,[||]) env in + let newenv = push_rec_types !evdref (names,ftys,[||]) env in let vdefj = Array.map2_i (fun i ctxt def -> @@ -641,7 +641,7 @@ let rec pretype k0 resolve_tc (tycon : type_constraint) (env : ExtraEnv.t) evdre let (ctxt,ty) = decompose_prod_n_assum !evdref (Context.Rel.length ctxt) (lift nbfix ftys.(i)) in - let nenv = push_rel_context ctxt newenv in + let nenv = push_rel_context !evdref ctxt newenv in let j = pretype (mk_tycon ty) nenv evdref lvar def in { uj_val = it_mkLambda_or_LetIn j.uj_val ctxt; uj_type = it_mkProd_or_LetIn j.uj_type ctxt }) @@ -783,7 +783,7 @@ let rec pretype k0 resolve_tc (tycon : type_constraint) (env : ExtraEnv.t) evdre the substitution must also be applied on variables before they are looked up in the rel context. *) let var = LocalAssum (name, j.utj_val) in - let j' = pretype rng (push_rel var env) evdref lvar c2 in + let j' = pretype rng (push_rel !evdref var env) evdref lvar c2 in let name = ltac_interp_name lvar name in let resj = judge_of_abstraction env.ExtraEnv.env (orelse_name name name') j j' in inh_conv_coerce_to_tycon loc env evdref resj tycon @@ -799,7 +799,7 @@ let rec pretype k0 resolve_tc (tycon : type_constraint) (env : ExtraEnv.t) evdre { j with utj_val = lift 1 j.utj_val } | Name _ -> let var = LocalAssum (name, j.utj_val) in - let env' = push_rel var env in + let env' = push_rel !evdref var env in pretype_type empty_valcon env' evdref lvar c2 in let name = ltac_interp_name lvar name in @@ -828,7 +828,7 @@ let rec pretype k0 resolve_tc (tycon : type_constraint) (env : ExtraEnv.t) evdre looked up in the rel context. *) let var = LocalDef (name, j.uj_val, t) in let tycon = lift_tycon 1 tycon in - let j' = pretype tycon (push_rel var env) evdref lvar c2 in + let j' = pretype tycon (push_rel !evdref var env) evdref lvar c2 in let name = ltac_interp_name lvar name in { uj_val = mkLetIn (name, j.uj_val, t, j'.uj_val) ; uj_type = subst1 j.uj_val j'.uj_type } @@ -877,7 +877,7 @@ let rec pretype k0 resolve_tc (tycon : type_constraint) (env : ExtraEnv.t) evdre mkCase (ci, p, cj.uj_val,[|f|]) else it_mkLambda_or_LetIn f fsign in - let env_f = push_rel_context fsign env in + let env_f = push_rel_context !evdref fsign env in (* Make dependencies from arity signature impossible *) let arsgn = let arsgn,_ = get_arity env.ExtraEnv.env indf in @@ -890,11 +890,10 @@ let rec pretype k0 resolve_tc (tycon : type_constraint) (env : ExtraEnv.t) evdre let nar = List.length arsgn in (match po with | Some p -> - let env_p = push_rel_context psign env in + let env_p = push_rel_context !evdref psign env in let pj = pretype_type empty_valcon env_p evdref lvar p in let ccl = nf_evar !evdref pj.utj_val in - let psign = make_arity_signature env.ExtraEnv.env true indf in (* with names *) - let psign = List.map (fun d -> map_rel_decl EConstr.of_constr d) psign in + let psign = make_arity_signature env.ExtraEnv.env !evdref true indf in (* with names *) let p = it_mkLambda_or_LetIn ccl psign in let inst = (Array.map_to_list EConstr.of_constr cs.cs_concl_realargs) @@ -951,7 +950,7 @@ let rec pretype k0 resolve_tc (tycon : type_constraint) (env : ExtraEnv.t) evdre let psign = List.map (fun d -> map_rel_decl EConstr.of_constr d) psign in let pred,p = match po with | Some p -> - let env_p = push_rel_context psign env in + let env_p = push_rel_context !evdref psign env in let pj = pretype_type empty_valcon env_p evdref lvar p in let ccl = nf_evar !evdref pj.utj_val in let pred = it_mkLambda_or_LetIn ccl psign in @@ -961,7 +960,7 @@ let rec pretype k0 resolve_tc (tycon : type_constraint) (env : ExtraEnv.t) evdre let p = match tycon with | Some ty -> ty | None -> - let env = ltac_interp_name_env k0 lvar env in + let env = ltac_interp_name_env k0 lvar env !evdref in new_type_evar env evdref loc in it_mkLambda_or_LetIn (lift (nar+1) p) psign, p in @@ -980,7 +979,7 @@ let rec pretype k0 resolve_tc (tycon : type_constraint) (env : ExtraEnv.t) evdre | Anonymous -> Name Namegen.default_non_dependent_ident)) cs_args in - let env_c = push_rel_context csgn env in + let env_c = push_rel_context !evdref csgn env in let bj = pretype (mk_tycon pi) env_c evdref lvar b in it_mkLambda_or_LetIn bj.uj_val cs_args in let b1 = f cstrs.(0) b1 in @@ -997,7 +996,7 @@ let rec pretype k0 resolve_tc (tycon : type_constraint) (env : ExtraEnv.t) evdre | GCases (loc,sty,po,tml,eqns) -> Cases.compile_cases loc sty - ((fun vtyc env evdref -> pretype vtyc (make_env env) evdref lvar),evdref) + ((fun vtyc env evdref -> pretype vtyc (make_env env !evdref) evdref lvar),evdref) tycon env.ExtraEnv.env (* loc *) (po,tml,eqns) | GCast (loc,c,k) -> @@ -1090,7 +1089,7 @@ and pretype_type k0 resolve_tc valcon (env : ExtraEnv.t) evdref lvar = function { utj_val = v; utj_type = s } | None -> - let env = ltac_interp_name_env k0 lvar env in + let env = ltac_interp_name_env k0 lvar env !evdref in let s = evd_comb0 (new_sort_variable univ_flexible_alg) evdref in { utj_val = e_new_evar env evdref ~src:(loc, knd) ~naming (mkSort s); utj_type = s}) @@ -1107,7 +1106,7 @@ and pretype_type k0 resolve_tc valcon (env : ExtraEnv.t) evdref lvar = function ~loc:(loc_of_glob_constr c) env.ExtraEnv.env !evdref tj.utj_val v let ise_pretype_gen flags env sigma lvar kind c = - let env = make_env env in + let env = make_env env sigma in let evdref = ref sigma in let k0 = Context.Rel.length (rel_context env) in let c' = match kind with @@ -1150,7 +1149,7 @@ let on_judgment sigma f j = {uj_val = c; uj_type = t} let understand_judgment env sigma c = - let env = make_env env in + let env = make_env env sigma in let evdref = ref sigma in let k0 = Context.Rel.length (rel_context env) in let j = pretype k0 true empty_tycon env evdref empty_lvar c in @@ -1160,7 +1159,7 @@ let understand_judgment env sigma c = in j, Evd.evar_universe_context !evdref let understand_judgment_tcc env evdref c = - let env = make_env env in + let env = make_env env !evdref in let k0 = Context.Rel.length (rel_context env) in let j = pretype k0 true empty_tycon env evdref empty_lvar c in on_judgment !evdref (fun c -> @@ -1217,7 +1216,7 @@ let type_uconstr ?(flags = constr_flags) end } let pretype k0 resolve_tc typcon env evdref lvar t = - pretype k0 resolve_tc typcon (make_env env) evdref lvar t + pretype k0 resolve_tc typcon (make_env env !evdref) evdref lvar t let pretype_type k0 resolve_tc valcon env evdref lvar t = - pretype_type k0 resolve_tc valcon (make_env env) evdref lvar t + pretype_type k0 resolve_tc valcon (make_env env !evdref) evdref lvar t diff --git a/pretyping/tacred.ml b/pretyping/tacred.ml index 9f3f3c7e5..ef9f39d77 100644 --- a/pretyping/tacred.ml +++ b/pretyping/tacred.ml @@ -1141,7 +1141,7 @@ let compute = cbv_betadeltaiota let abstract_scheme env sigma (locc,a) (c, sigma) = let ta = Retyping.get_type_of env sigma a in - let na = named_hd env (EConstr.to_constr sigma ta) Anonymous in + let na = named_hd env sigma ta Anonymous in if occur_meta sigma ta then error "Cannot find a type for the generalisation."; if occur_meta sigma a then mkLambda (na,ta,c), sigma diff --git a/pretyping/typing.ml b/pretyping/typing.ml index bdd3663d1..dec22ecd0 100644 --- a/pretyping/typing.ml +++ b/pretyping/typing.ml @@ -92,8 +92,7 @@ let max_sort l = if Sorts.List.mem InSet l then InSet else InProp let e_is_correct_arity env evdref c pj ind specif params = - let arsign = make_arity_signature env true (make_ind_family (ind,params)) in - let arsign = List.map (fun d -> Termops.map_rel_decl EConstr.of_constr d) arsign in + let arsign = make_arity_signature env !evdref true (make_ind_family (ind,params)) in let allowed_sorts = elim_sorts specif in let error () = Pretype_errors.error_elim_arity env !evdref ind allowed_sorts c pj None in let rec srec env pt ar = diff --git a/pretyping/unification.ml b/pretyping/unification.ml index 589201fe2..baa12db08 100644 --- a/pretyping/unification.ml +++ b/pretyping/unification.ml @@ -85,7 +85,7 @@ let occur_meta_evd sigma mv c = let abstract_scheme env evd c l lname_typ = let mkLambda_name env (n,a,b) = - mkLambda (named_hd env (EConstr.Unsafe.to_constr a) n, a, b) + mkLambda (named_hd env evd a n, a, b) in List.fold_left2 (fun (t,evd) (locc,a) decl -> @@ -1617,8 +1617,7 @@ let make_eq_test env evd c = let make_abstraction_core name (test,out) env sigma c ty occs check_occs concl = let id = let t = match ty with Some t -> t | None -> get_type_of env sigma c in - let t = EConstr.Unsafe.to_constr t in - let x = id_of_name_using_hdchar (Global.env()) t name in + let x = id_of_name_using_hdchar (Global.env()) sigma t name in let ids = ids_of_named_context (named_context env) in if name == Anonymous then next_ident_away_in_goal x ids else if mem_named_context_val x (named_context_val env) then diff --git a/printing/printer.ml b/printing/printer.ml index c7d3a1ba3..447337b9a 100644 --- a/printing/printer.ml +++ b/printing/printer.ml @@ -515,7 +515,7 @@ let print_evar_constraints gl sigma = problem. MS: we should rather stop depending on anonymous variables, they can be used to indicate independency. Also, this depends on a strategy for naming/renaming *) - Namegen.make_all_name_different env in + Namegen.make_all_name_different env sigma in str" " ++ hov 2 (pr_env env ++ pr_leconstr_env env sigma t1 ++ spc () ++ str (match pbty with diff --git a/proofs/clenv.ml b/proofs/clenv.ml index e580bccc3..5645850b2 100644 --- a/proofs/clenv.ml +++ b/proofs/clenv.ml @@ -555,7 +555,7 @@ let make_clenv_binding_gen hyps_only n env sigma (c,t) = function let clause = mk_clenv_from_env env sigma n (c,t) in clenv_constrain_dep_args hyps_only largs clause | ExplicitBindings lbind -> - let t = EConstr.of_constr (rename_bound_vars_as_displayed [] [] (EConstr.Unsafe.to_constr t)) in + let t = rename_bound_vars_as_displayed sigma [] [] t in let clause = mk_clenv_from_env env sigma n (c, t) in clenv_match_args lbind clause @@ -603,9 +603,7 @@ let make_evar_clause env sigma ?len t = | Some n -> assert (0 <= n); n in (** FIXME: do the renaming online *) - let t = EConstr.Unsafe.to_constr t in - let t = rename_bound_vars_as_displayed [] [] t in - let t = EConstr.of_constr t in + let t = rename_bound_vars_as_displayed sigma [] [] t in let rec clrec (sigma, holes) n t = if n = 0 then (sigma, holes, t) else match EConstr.kind sigma t with diff --git a/tactics/class_tactics.ml b/tactics/class_tactics.ml index 55fda1c7d..669d80814 100644 --- a/tactics/class_tactics.ml +++ b/tactics/class_tactics.ml @@ -1458,7 +1458,7 @@ let _ = Hook.set Typeclasses.solve_all_instances_hook solve_inst let resolve_one_typeclass env ?(sigma=Evd.empty) gl unique = - let nc, gl, subst, _, _ = Evarutil.push_rel_context_to_named_context env gl in + let nc, gl, subst, _, _ = Evarutil.push_rel_context_to_named_context env sigma gl in let (gl,t,sigma) = Goal.V82.mk_goal sigma nc gl Store.empty in let (ev, _) = destEvar sigma t in diff --git a/tactics/eqschemes.ml b/tactics/eqschemes.ml index 188e215a5..b08456f2f 100644 --- a/tactics/eqschemes.ml +++ b/tactics/eqschemes.ml @@ -76,10 +76,24 @@ let build_dependent_inductive ind (mib,mip) = Context.Rel.to_extended_list mkRel mip.mind_nrealdecls mib.mind_params_ctxt @ Context.Rel.to_extended_list mkRel 0 realargs) +let named_hd env t na = named_hd env Evd.empty (EConstr.of_constr t) na +let name_assumption env = function +| LocalAssum (na,t) -> LocalAssum (named_hd env t na, t) +| LocalDef (na,c,t) -> LocalDef (named_hd env c na, c, t) + +let name_context env hyps = + snd + (List.fold_left + (fun (env,hyps) d -> + let d' = name_assumption env d in (push_rel d' env, d' :: hyps)) + (env,[]) (List.rev hyps)) + let my_it_mkLambda_or_LetIn s c = it_mkLambda_or_LetIn c s let my_it_mkProd_or_LetIn s c = Term.it_mkProd_or_LetIn c s let my_it_mkLambda_or_LetIn_name s c = - it_mkLambda_or_LetIn_name (Global.env()) c s + let env = Global.env () in + let mkLambda_or_LetIn_name d b = mkLambda_or_LetIn (name_assumption env d) b in + List.fold_left (fun c d -> mkLambda_or_LetIn_name d c) c s let get_coq_eq ctx = try diff --git a/tactics/equality.ml b/tactics/equality.ml index 7f7a07b8f..d9b668517 100644 --- a/tactics/equality.ml +++ b/tactics/equality.ml @@ -857,14 +857,13 @@ let descend_then env sigma head dirn = (dirn_nlams, dirn_env, (fun dirnval (dfltval,resty) -> - let deparsign = make_arity_signature env true indf in - let deparsign = List.map (fun d -> map_rel_decl EConstr.of_constr d) deparsign in + let deparsign = make_arity_signature env sigma true indf in let p = it_mkLambda_or_LetIn (lift (mip.mind_nrealargs+1) resty) deparsign in let build_branch i = let result = if Int.equal i dirn then dirnval else dfltval in - let args = name_context env cstr.(i-1).cs_args in - let args = List.map (fun d -> map_rel_decl EConstr.of_constr d) args in + let cs_args = List.map (fun d -> map_rel_decl EConstr.of_constr d) cstr.(i-1).cs_args in + let args = name_context env sigma cs_args in it_mkLambda_or_LetIn result args in let brl = List.map build_branch @@ -905,8 +904,7 @@ let build_selector env sigma dirn c ind special default = let ind, _ = check_privacy env indp in let typ = Retyping.get_type_of env sigma default in let (mib,mip) = lookup_mind_specif env ind in - let deparsign = make_arity_signature env true indf in - let deparsign = List.map (fun d -> map_rel_decl EConstr.of_constr d) deparsign in + let deparsign = make_arity_signature env sigma true indf in let p = it_mkLambda_or_LetIn typ deparsign in let cstrs = get_constructors env indf in let build_branch i = @@ -1535,9 +1533,6 @@ let decomp_tuple_term env sigma c t = in [((ex,exty),inner_code)]::iterated_decomp in decomprec (mkRel 1) c t -let lambda_create env (a,b) = - mkLambda (named_hd env (EConstr.Unsafe.to_constr a) Anonymous, a, b) - let subst_tuple_term env sigma dep_pair1 dep_pair2 b = let sigma = Sigma.to_evar_map sigma in let typ = get_type_of env sigma dep_pair1 in @@ -1555,9 +1550,9 @@ let subst_tuple_term env sigma dep_pair1 dep_pair2 b = (* We build the expected goal *) let abst_B = List.fold_right - (fun (e,t) body -> lambda_create env (t,subst_term sigma e body)) e1_list b in + (fun (e,t) body -> lambda_create env sigma (t,subst_term sigma e body)) e1_list b in let pred_body = beta_applist sigma (abst_B,proj_list) in - let body = mkApp (lambda_create env (typ,pred_body),[|dep_pair1|]) in + let body = mkApp (lambda_create env sigma (typ,pred_body),[|dep_pair1|]) in let expected_goal = beta_applist sigma (abst_B,List.map fst e2_list) in (* Simulate now the normalisation treatment made by Logic.mk_refgoals *) let expected_goal = nf_betaiota sigma expected_goal in diff --git a/tactics/inv.ml b/tactics/inv.ml index ecb8eedac..632a29721 100644 --- a/tactics/inv.ml +++ b/tactics/inv.ml @@ -90,8 +90,7 @@ let make_inv_predicate env evd indf realargs id status concl = | None -> let sort = get_sort_family_of env !evd concl in let sort = Evarutil.evd_comb1 (Evd.fresh_sort_in_family env) evd sort in - let p = make_arity env true indf sort in - let p = EConstr.of_constr p in + let p = make_arity env !evd true indf sort in let evd',(p,ptyp) = Unification.abstract_list_all env !evd p concl (realargs@[mkVar id]) in evd := evd'; p in @@ -133,11 +132,7 @@ let make_inv_predicate env evd indf realargs id status concl = build_concl eqns args (succ n) restlist in let (newconcl, args) = build_concl [] [] 0 realargs in - let name_context env ctx = - let map f c = List.map (fun d -> Termops.map_rel_decl f d) c in - map EConstr.of_constr (name_context env (map EConstr.Unsafe.to_constr ctx)) - in - let predicate = it_mkLambda_or_LetIn newconcl (name_context env hyps) in + let predicate = it_mkLambda_or_LetIn newconcl (name_context env !evd hyps) in let _ = Evarutil.evd_comb1 (Typing.type_of env) evd predicate in (* OK - this predicate should now be usable by res_elimination_then to do elimination on the conclusion. *) diff --git a/tactics/leminv.ml b/tactics/leminv.ml index d7c396179..d864e547c 100644 --- a/tactics/leminv.ml +++ b/tactics/leminv.ml @@ -119,11 +119,11 @@ let max_prefix_sign lid sign = let rec add_prods_sign env sigma t = match EConstr.kind sigma (whd_all env sigma t) with | Prod (na,c1,b) -> - let id = id_of_name_using_hdchar env (EConstr.Unsafe.to_constr t) na in + let id = id_of_name_using_hdchar env sigma t na in let b'= subst1 (mkVar id) b in add_prods_sign (push_named (LocalAssum (id,c1)) env) sigma b' | LetIn (na,c1,t1,b) -> - let id = id_of_name_using_hdchar env (EConstr.Unsafe.to_constr t) na in + let id = id_of_name_using_hdchar env sigma t na in let b'= subst1 (mkVar id) b in add_prods_sign (push_named (LocalDef (id,c1,t1)) env) sigma b' | _ -> (env,t) @@ -147,8 +147,7 @@ let compute_first_inversion_scheme env sigma ind sort dep_option = let p = next_ident_away (Id.of_string "P") allvars in let pty,goal = if dep_option then - let pty = make_arity env true indf sort in - let pty = EConstr.of_constr pty in + let pty = make_arity env sigma true indf sort in let goal = mkProd (Anonymous, mkAppliedInd ind, applist(mkVar p,realargs@[mkRel 1])) diff --git a/tactics/tactics.ml b/tactics/tactics.ml index a29803251..13ffbc52f 100644 --- a/tactics/tactics.ml +++ b/tactics/tactics.ml @@ -412,16 +412,13 @@ let id_of_name_with_default id = function let default_id_of_sort s = if Sorts.is_small s then default_small_ident else default_type_ident -let id_of_name_using_hdchar env c name = - id_of_name_using_hdchar env (EConstr.Unsafe.to_constr c) name - let default_id env sigma decl = let open Context.Rel.Declaration in match decl with | LocalAssum (name,t) -> let dft = default_id_of_sort (Retyping.get_sort_of env sigma t) in id_of_name_with_default dft name - | LocalDef (name,b,_) -> id_of_name_using_hdchar env b name + | LocalDef (name,b,_) -> id_of_name_using_hdchar env sigma b name (* Non primitive introduction tactics are treated by intro_then_gen There is possibly renaming, with possibly names to avoid and @@ -1075,14 +1072,14 @@ let intros_replacing ids = (* User-level introduction tactics *) -let lookup_hypothesis_as_renamed env ccl = function - | AnonHyp n -> Detyping.lookup_index_as_renamed env (EConstr.Unsafe.to_constr ccl) n - | NamedHyp id -> Detyping.lookup_name_as_displayed env (EConstr.Unsafe.to_constr ccl) id +let lookup_hypothesis_as_renamed env sigma ccl = function + | AnonHyp n -> Detyping.lookup_index_as_renamed env sigma ccl n + | NamedHyp id -> Detyping.lookup_name_as_displayed env sigma ccl id let lookup_hypothesis_as_renamed_gen red h gl = let env = Proofview.Goal.env gl in let rec aux ccl = - match lookup_hypothesis_as_renamed env ccl h with + match lookup_hypothesis_as_renamed env (Tacmach.New.project gl) ccl h with | None when red -> let (redfun, _) = Redexpr.reduction_of_red_expr env (Red true) in let Sigma (c, _, _) = redfun.e_redfun env (Proofview.Goal.sigma gl) ccl in @@ -1350,7 +1347,7 @@ let enforce_prop_bound_names rename tac = if Retyping.get_sort_family_of env sigma t = InProp then (* "very_standard" says that we should have "H" names only, but this would break compatibility even more... *) - let s = match Namegen.head_name (EConstr.Unsafe.to_constr t) with + let s = match Namegen.head_name sigma t with | Some id when not very_standard -> string_of_id id | _ -> "" in Name (add_suffix Namegen.default_prop_ident s) @@ -2768,7 +2765,7 @@ let enough_by na t tac = forward false (Some (Some tac)) (ipat_of_name na) t (* Compute a name for a generalization *) -let generalized_name sigma c t ids cl = function +let generalized_name env sigma c t ids cl = function | Name id as na -> if Id.List.mem id ids then user_err (pr_id id ++ str " is already used."); @@ -2783,7 +2780,7 @@ let generalized_name sigma c t ids cl = function (* On ne s'etait pas casse la tete : on avait pris pour nom de variable la premiere lettre du type, meme si "c" avait ete une constante dont on aurait pu prendre directement le nom *) - named_hd (Global.env()) (EConstr.Unsafe.to_constr t) Anonymous + named_hd env sigma t Anonymous (* Abstract over [c] in [forall x1:A1(c)..xi:Ai(c).T(c)] producing [forall x, x1:A1(x1), .., xi:Ai(x). T(x)] with all [c] abtracted in [Ai] @@ -2795,7 +2792,7 @@ let generalize_goal_gen env sigma ids i ((occs,c,b),na) t cl = let dummy_prod = it_mkProd_or_LetIn mkProp decls in let newdecls,_ = decompose_prod_n_assum sigma i (subst_term_gen sigma EConstr.eq_constr_nounivs c dummy_prod) in let cl',sigma' = subst_closed_term_occ env sigma (AtOccs occs) c (it_mkProd_or_LetIn cl newdecls) in - let na = generalized_name sigma c t ids cl' na in + let na = generalized_name env sigma c t ids cl' na in let decl = match b with | None -> LocalAssum (na,t) | Some b -> LocalDef (na,b,t) @@ -3230,7 +3227,7 @@ let atomize_param_of_ind_then (indref,nparams,_) hyp0 tac = | Var id -> id | _ -> let type_of = Tacmach.New.pf_unsafe_type_of gl in - id_of_name_using_hdchar (Global.env()) (type_of c) Anonymous in + id_of_name_using_hdchar (Global.env()) sigma (type_of c) Anonymous in let x = fresh_id_in_env avoid id env in Tacticals.New.tclTHEN (letin_tac None (Name x) c None allHypsAndConcl) @@ -4434,7 +4431,7 @@ let induction_gen clear_flag isrec with_evars elim declaring the induction argument as a new local variable *) let id = (* Type not the right one if partially applied but anyway for internal use*) - let x = id_of_name_using_hdchar (Global.env()) t Anonymous in + let x = id_of_name_using_hdchar (Global.env()) evd t Anonymous in new_fresh_id [] x gl in let info_arg = (is_arg_pure_hyp, not enough_applied) in pose_induction_arg_then @@ -4471,7 +4468,7 @@ let induction_gen_l isrec with_evars elim names lc = let type_of = Tacmach.New.pf_unsafe_type_of gl in let sigma = Tacmach.New.project gl in let x = - id_of_name_using_hdchar (Global.env()) (type_of c) Anonymous in + id_of_name_using_hdchar (Global.env()) sigma (type_of c) Anonymous in let id = new_fresh_id [] x gl in let newl' = List.map (fun r -> replace_term sigma c (mkVar id) r) l' in diff --git a/test-suite/output/inference.out b/test-suite/output/inference.out index 576fbd7c0..c0eede99e 100644 --- a/test-suite/output/inference.out +++ b/test-suite/output/inference.out @@ -6,13 +6,13 @@ fun e : option L => match e with : option L -> option L fun (m n p : nat) (H : S m <= S n + p) => le_S_n m (n + p) H : forall m n p : nat, S m <= S n + p -> m <= n + p -fun n : nat => let x := A n : T n in ?y ?y0 : T n +fun n : nat => let x := A n : T n in ?t ?y : T n : forall n : nat, T n where -?y : [n : nat x := A n : T n |- ?T -> T n] -?y0 : [n : nat x := A n : T n |- ?T] -fun n : nat => ?y ?y0 : T n +?t : [n : nat x := A n : T n |- ?T -> T n] +?y : [n : nat x := A n : T n |- ?T] +fun n : nat => ?t ?y : T n : forall n : nat, T n where -?y : [n : nat |- ?T -> T n] -?y0 : [n : nat |- ?T] +?t : [n : nat |- ?T -> T n] +?y : [n : nat |- ?T] diff --git a/toplevel/himsg.ml b/toplevel/himsg.ml index 6982205fd..dea1f22d9 100644 --- a/toplevel/himsg.ml +++ b/toplevel/himsg.ml @@ -39,7 +39,7 @@ let contract env sigma lc = env | _ -> let t = Vars.substl !l (RelDecl.get_type decl) in - let decl = decl |> RelDecl.map_name (named_hd env (EConstr.Unsafe.to_constr t)) |> RelDecl.map_value (Vars.substl !l) |> RelDecl.set_type t in + let decl = decl |> RelDecl.map_name (named_hd env sigma t) |> RelDecl.map_value (Vars.substl !l) |> RelDecl.set_type t in l := (mkRel 1) :: List.map (Vars.lift 1) !l; push_rel decl env in @@ -206,7 +206,7 @@ let pr_puniverses f env (c,u) = let explain_elim_arity env sigma ind sorts c pj okinds = let open EConstr in - let env = make_all_name_different env in + let env = make_all_name_different env sigma in let pi = pr_inductive env (fst ind) in let pc = pr_leconstr_env env sigma c in let msg = match okinds with @@ -241,7 +241,7 @@ let explain_elim_arity env sigma ind sorts c pj okinds = let explain_case_not_inductive env sigma cj = let cj = Evarutil.j_nf_evar sigma cj in - let env = make_all_name_different env in + let env = make_all_name_different env sigma in let pc = pr_leconstr_env env sigma cj.uj_val in let pct = pr_leconstr_env env sigma cj.uj_type in match EConstr.kind sigma cj.uj_type with @@ -254,7 +254,7 @@ let explain_case_not_inductive env sigma cj = let explain_number_branches env sigma cj expn = let cj = Evarutil.j_nf_evar sigma cj in - let env = make_all_name_different env in + let env = make_all_name_different env sigma in let pc = pr_leconstr_env env sigma cj.uj_val in let pct = pr_leconstr_env env sigma cj.uj_type in str "Matching on term" ++ brk(1,1) ++ pc ++ spc () ++ @@ -263,7 +263,7 @@ let explain_number_branches env sigma cj expn = let explain_ill_formed_branch env sigma c ci actty expty = let simp t = Reductionops.nf_betaiota sigma (Evarutil.nf_evar sigma t) in - let env = make_all_name_different env in + let env = make_all_name_different env sigma in let pc = pr_leconstr_env env sigma c in let pa, pe = pr_explicit env sigma (simp actty) (simp expty) in strbrk "In pattern-matching on term" ++ brk(1,1) ++ pc ++ @@ -300,7 +300,7 @@ let explain_unification_error env sigma p1 p2 = function (* Error speaks from itself *) [] | ConversionFailed (env,t1,t2) -> if EConstr.eq_constr sigma t1 p1 && EConstr.eq_constr sigma t2 p2 then [] else - let env = make_all_name_different env in + let env = make_all_name_different env sigma in let t1 = Evarutil.nf_evar sigma t1 in let t2 = Evarutil.nf_evar sigma t2 in if not (EConstr.eq_constr sigma t1 p1) || not (EConstr.eq_constr sigma t2 p2) then @@ -328,7 +328,7 @@ let explain_unification_error env sigma p1 p2 = function let u = EConstr.of_constr u in let t = Evarutil.nf_evar sigma t in let u = Evarutil.nf_evar sigma u in - let env = make_all_name_different env in + let env = make_all_name_different env sigma in (strbrk "cannot satisfy constraint " ++ pr_leconstr_env env sigma t ++ str " == " ++ pr_leconstr_env env sigma u) :: aux t u e @@ -341,7 +341,7 @@ let explain_unification_error env sigma p1 p2 = function prlist_with_sep pr_semicolon (fun x -> x) l ++ str ")" let explain_actual_type env sigma j t reason = - let env = make_all_name_different env in + let env = make_all_name_different env sigma in let j = j_nf_betaiotaevar sigma j in let t = Reductionops.nf_betaiota sigma t in (** Actually print *) @@ -361,7 +361,7 @@ let explain_cant_apply_bad_type env sigma (n,exptyp,actualtyp) rator randl = let exptyp = Evarutil.nf_evar sigma exptyp in let actualtyp = Reductionops.nf_betaiota sigma actualtyp in let rator = Evarutil.j_nf_evar sigma rator in - let env = make_all_name_different env in + let env = make_all_name_different env sigma in let actualtyp, exptyp = pr_explicit env sigma actualtyp exptyp in let nargs = Array.length randl in (* let pe = pr_ne_context_of (str "in environment") env sigma in*) @@ -387,7 +387,7 @@ let explain_cant_apply_bad_type env sigma (n,exptyp,actualtyp) rator randl = let explain_cant_apply_not_functional env sigma rator randl = let randl = Evarutil.jv_nf_evar sigma randl in let rator = Evarutil.j_nf_evar sigma rator in - let env = make_all_name_different env in + let env = make_all_name_different env sigma in let nargs = Array.length randl in (* let pe = pr_ne_context_of (str "in environment") env sigma in*) let pr = pr_leconstr_env env sigma rator.uj_val in @@ -437,7 +437,7 @@ let explain_ill_formed_rec_body env sigma err names i fixenv vdefj = str "Recursive definition on" ++ spc () ++ pr_lconstr_env env sigma c ++ spc () ++ str "which should be an inductive type" | RecursionOnIllegalTerm(j,(arg_env, arg),le,lt) -> - let arg_env = make_all_name_different arg_env in + let arg_env = make_all_name_different arg_env sigma in let called = match names.(j) with Name id -> pr_id id @@ -503,7 +503,7 @@ let explain_ill_formed_rec_body env sigma err names i fixenv vdefj = pr_ne_context_of (str "In environment") env sigma ++ st ++ str "." ++ fnl () ++ (try (* May fail with unresolved globals. *) - let fixenv = make_all_name_different fixenv in + let fixenv = make_all_name_different fixenv sigma in let pvd = pr_lconstr_env fixenv sigma vdefj.(i).uj_val in str"Recursive definition is:" ++ spc () ++ pvd ++ str "." with e when CErrors.noncritical e -> mt ()) @@ -511,7 +511,7 @@ let explain_ill_formed_rec_body env sigma err names i fixenv vdefj = let explain_ill_typed_rec_body env sigma i names vdefj vargs = let vdefj = Evarutil.jv_nf_evar sigma vdefj in let vargs = Array.map (Evarutil.nf_evar sigma) vargs in - let env = make_all_name_different env in + let env = make_all_name_different env sigma in let pvd = pr_leconstr_env env sigma vdefj.(i).uj_val in let pvdt, pv = pr_explicit env sigma vdefj.(i).uj_type vargs.(i) in str "The " ++ @@ -521,13 +521,13 @@ let explain_ill_typed_rec_body env sigma i names vdefj vargs = str "while it should be" ++ spc () ++ pv ++ str "." let explain_cant_find_case_type env sigma c = - let env = make_all_name_different env in + let env = make_all_name_different env sigma in let pe = pr_leconstr_env env sigma c in str "Cannot infer the return type of pattern-matching on" ++ ws 1 ++ pe ++ str "." let explain_occur_check env sigma ev rhs = - let env = make_all_name_different env in + let env = make_all_name_different env sigma in let pt = pr_leconstr_env env sigma rhs in str "Cannot define " ++ pr_existential_key sigma ev ++ str " with term" ++ brk(1,1) ++ pt ++ spc () ++ str "that would depend on itself." @@ -624,7 +624,7 @@ let explain_wrong_case_info env (ind,u) ci = spc () ++ pc ++ str "." let explain_cannot_unify env sigma m n e = - let env = make_all_name_different env in + let env = make_all_name_different env sigma in let m = Evarutil.nf_evar sigma m in let n = Evarutil.nf_evar sigma n in let pm, pn = pr_explicit env sigma m n in @@ -695,7 +695,7 @@ let explain_unsatisfied_constraints env sigma cst = spc () ++ str "(maybe a bugged tactic)." let explain_type_error env sigma err = - let env = make_all_name_different env in + let env = make_all_name_different env sigma in match err with | UnboundRel n -> explain_unbound_rel env sigma n @@ -774,7 +774,7 @@ let pr_constraints printenv env sigma evars cstrs = (fun (ev, evi) -> fnl () ++ pr_existential_key sigma ev ++ str " : " ++ pr_lconstr_env env' sigma evi.evar_concl ++ fnl ()) l in - h 0 (pe ++ evs ++ pr_evar_constraints cstrs) + h 0 (pe ++ evs ++ pr_evar_constraints sigma cstrs) else let filter evk _ = Evar.Map.mem evk evars in pr_evar_map_filter ~with_univs:false filter sigma @@ -810,7 +810,7 @@ let explain_unsatisfiable_constraints env sigma constr comp = let explain_pretype_error env sigma err = let env = Evardefine.env_nf_betaiotaevar sigma env in - let env = make_all_name_different env in + let env = make_all_name_different env sigma in match err with | CantFindCaseType c -> explain_cant_find_case_type env sigma c | ActualTypeNotCoercible (j,t,e) -> @@ -1210,7 +1210,7 @@ let explain_recursion_scheme_error = function let explain_bad_pattern env sigma cstr ty = let ty = EConstr.to_constr sigma ty in - let env = make_all_name_different env in + let env = make_all_name_different env sigma in let pt = pr_lconstr_env env sigma ty in let pc = pr_constructor env cstr in str "Found the constructor " ++ pc ++ brk(1,1) ++ @@ -1255,7 +1255,7 @@ let explain_non_exhaustive env pats = let explain_cannot_infer_predicate env sigma typs = let inj c = EConstr.to_constr sigma c in let typs = Array.map_to_list (fun (c1, c2) -> (inj c1, inj c2)) typs in - let env = make_all_name_different env in + let env = make_all_name_different env sigma in let pr_branch (cstr,typ) = let cstr,_ = decompose_app cstr in str "For " ++ pr_lconstr_env env sigma cstr ++ str ": " ++ pr_lconstr_env env sigma typ diff --git a/toplevel/vernacentries.ml b/toplevel/vernacentries.ml index 55477cbcf..43ffa9ef3 100644 --- a/toplevel/vernacentries.ml +++ b/toplevel/vernacentries.ml @@ -1237,7 +1237,7 @@ let vernac_reserve bl = let env = Global.env() in let sigma = Evd.from_env env in let t,ctx = Constrintern.interp_type env sigma c in - let t = Detyping.detype false [] env (Evd.from_ctx ctx) t in + let t = Detyping.detype false [] env (Evd.from_ctx ctx) (EConstr.of_constr t) in let t,_ = Notation_ops.notation_constr_of_glob_constr (default_env ()) t in Reserve.declare_reserved_type idl t) in List.iter sb_decl bl |