From e759333a8b5c11247c4cc134fdde8c1bd85a6e17 Mon Sep 17 00:00:00 2001 From: Matthieu Sozeau Date: Fri, 11 Sep 2015 18:07:39 +0200 Subject: Universes: enforce Set <= i for all Type occurrences. --- pretyping/evd.ml | 41 +++++++++++++++++++++++++++-------------- pretyping/evd.mli | 6 +++--- 2 files changed, 30 insertions(+), 17 deletions(-) (limited to 'pretyping') diff --git a/pretyping/evd.ml b/pretyping/evd.ml index 6326112912..fe5f12dd8a 100644 --- a/pretyping/evd.ml +++ b/pretyping/evd.ml @@ -453,7 +453,7 @@ let add_constraints_context ctx cstrs = in { ctx with uctx_local = (univs, Univ.Constraint.union local local'); uctx_univ_variables = vars; - uctx_universes = Univ.merge_constraints cstrs ctx.uctx_universes } + uctx_universes = Univ.merge_constraints local' ctx.uctx_universes } (* let addconstrkey = Profile.declare_profile "add_constraints_context";; *) (* let add_constraints_context = Profile.profile2 addconstrkey add_constraints_context;; *) @@ -1058,36 +1058,49 @@ let with_context_set rigid d (a, ctx) = let add_uctx_names s l (names, names_rev) = (UNameMap.add s l names, Univ.LMap.add l s names_rev) -let uctx_new_univ_variable rigid name +let uctx_new_univ_variable rigid name predicative ({ uctx_local = ctx; uctx_univ_variables = uvars; uctx_univ_algebraic = avars} as uctx) = let u = Universes.new_univ_level (Global.current_dirpath ()) in let ctx' = Univ.ContextSet.add_universe u ctx in - let uctx' = + let uctx', pred = match rigid with - | UnivRigid -> uctx + | UnivRigid -> uctx, true | UnivFlexible b -> let uvars' = Univ.LMap.add u None uvars in if b then {uctx with uctx_univ_variables = uvars'; - uctx_univ_algebraic = Univ.LSet.add u avars} - else {uctx with uctx_univ_variables = Univ.LMap.add u None uvars} in + uctx_univ_algebraic = Univ.LSet.add u avars}, false + else {uctx with uctx_univ_variables = uvars'}, false + in + (* let ctx' = *) + (* if pred then *) + (* Univ.ContextSet.add_constraints *) + (* (Univ.Constraint.singleton (Univ.Level.set, Univ.Le, u)) ctx' *) + (* else ctx' *) + (* in *) let names = match name with | Some n -> add_uctx_names n u uctx.uctx_names | None -> uctx.uctx_names in + let initial = + Univ.add_universe u pred uctx.uctx_initial_universes + in + let uctx' = {uctx' with uctx_names = names; uctx_local = ctx'; - uctx_universes = Univ.add_universe u uctx.uctx_universes}, u - -let new_univ_level_variable ?name rigid evd = - let uctx', u = uctx_new_univ_variable rigid name evd.universes in + uctx_universes = Univ.add_universe u pred uctx.uctx_universes; + uctx_initial_universes = initial} + in uctx', u + +let new_univ_level_variable ?name ?(predicative=true) rigid evd = + let uctx', u = uctx_new_univ_variable rigid name predicative evd.universes in ({evd with universes = uctx'}, u) -let new_univ_variable ?name rigid evd = - let uctx', u = uctx_new_univ_variable rigid name evd.universes in +let new_univ_variable ?name ?(predicative=true) rigid evd = + let uctx', u = uctx_new_univ_variable rigid name predicative evd.universes in ({evd with universes = uctx'}, Univ.Universe.make u) -let new_sort_variable ?name rigid d = - let (d', u) = new_univ_variable rigid ?name d in +let new_sort_variable ?name ?(predicative=true) rigid d = + let (d', u) = new_univ_variable rigid ?name ~predicative d in (d', Type u) let make_flexible_variable evd b u = diff --git a/pretyping/evd.mli b/pretyping/evd.mli index 94d9d5f662..c2ccc6d21a 100644 --- a/pretyping/evd.mli +++ b/pretyping/evd.mli @@ -505,9 +505,9 @@ val normalize_evar_universe_context_variables : evar_universe_context -> val normalize_evar_universe_context : evar_universe_context -> evar_universe_context -val new_univ_level_variable : ?name:string -> rigid -> evar_map -> evar_map * Univ.universe_level -val new_univ_variable : ?name:string -> rigid -> evar_map -> evar_map * Univ.universe -val new_sort_variable : ?name:string -> rigid -> evar_map -> evar_map * sorts +val new_univ_level_variable : ?name:string -> ?predicative:bool -> rigid -> evar_map -> evar_map * Univ.universe_level +val new_univ_variable : ?name:string -> ?predicative:bool -> rigid -> evar_map -> evar_map * Univ.universe +val new_sort_variable : ?name:string -> ?predicative:bool -> rigid -> evar_map -> evar_map * sorts val make_flexible_variable : evar_map -> bool -> Univ.universe_level -> evar_map val is_sort_variable : evar_map -> sorts -> Univ.universe_level option (** [is_sort_variable evm s] returns [Some u] or [None] if [s] is -- cgit v1.2.3 From 79163d582abc2e22512f0924675b6b0f0928f0ef Mon Sep 17 00:00:00 2001 From: Matthieu Sozeau Date: Tue, 15 Sep 2015 18:31:44 +0200 Subject: Univs: Fix part of bug #4161 Rechecking applications built by evarconv's imitation. --- pretyping/evarsolve.ml | 43 +++++++++++++++++++++++++++++++++++++------ 1 file changed, 37 insertions(+), 6 deletions(-) (limited to 'pretyping') diff --git a/pretyping/evarsolve.ml b/pretyping/evarsolve.ml index ac1692f451..a2189d5e4f 100644 --- a/pretyping/evarsolve.ml +++ b/pretyping/evarsolve.ml @@ -107,6 +107,7 @@ let refresh_universes ?(inferred=false) ?(onlyalg=false) pbty env evd t = let get_type_of_refresh ?(polyprop=true) ?(lax=false) env sigma c = let ty = Retyping.get_type_of ~polyprop ~lax env sigma c in refresh_universes (Some false) env sigma ty + (************************) (* Unification results *) @@ -127,6 +128,32 @@ let add_conv_oriented_pb ?(tail=true) (pbty,env,t1,t2) evd = | Some false -> add_conv_pb ~tail (Reduction.CUMUL,env,t2,t1) evd | None -> add_conv_pb ~tail (Reduction.CONV,env,t1,t2) evd +(* We retype applications to ensure the universe constraints are collected *) + +let recheck_applications conv_algo env evdref t = + let rec aux env t = + match kind_of_term t with + | App (f, args) -> + let () = aux env f in + let fty = Retyping.get_type_of env !evdref f in + let argsty = Array.map (fun x -> aux env x; Retyping.get_type_of env !evdref x) args in + let rec aux i ty = + if i < Array.length argsty then + match kind_of_term (whd_betadeltaiota env !evdref ty) with + | Prod (na, dom, codom) -> + (match conv_algo env !evdref Reduction.CUMUL argsty.(i) dom with + | Success evd -> evdref := evd; + aux (succ i) (subst1 args.(i) codom) + | UnifFailure (evd, reason) -> + Pretype_errors.error_cannot_unify env evd ~reason (argsty.(i), dom)) + | _ -> assert false + else () + in aux 0 fty + | _ -> + iter_constr_with_full_binders (fun d env -> push_rel d env) aux env t + in aux env t + + (*------------------------------------* * Restricting existing evars * *------------------------------------*) @@ -1404,10 +1431,10 @@ let rec invert_definition conv_algo choose env evd pbty (evk,argsv as ev) rhs = evdref := restrict_evar evd (fst ev'') None (UpdateWith candidates); evar'') | None -> - (* Evar/Rigid problem (or assimilated if not normal): we "imitate" *) - map_constr_with_full_binders (fun d (env,k) -> push_rel d env, k+1) - imitate envk t in - + (* Evar/Rigid problem (or assimilated if not normal): we "imitate" *) + map_constr_with_full_binders (fun d (env,k) -> push_rel d env, k+1) + imitate envk t + in let rhs = whd_beta evd rhs (* heuristic *) in let fast rhs = let filter_ctxt = evar_filtered_context evi in @@ -1426,8 +1453,12 @@ let rec invert_definition conv_algo choose env evd pbty (evk,argsv as ev) rhs = in let body = if fast rhs then nf_evar evd rhs - else imitate (env,0) rhs - in (!evdref,body) + else + let t' = imitate (env,0) rhs in + if !progress then + (recheck_applications conv_algo (evar_env evi) evdref t'; t') + else t' + in (!evdref,body) (* [define] tries to solve the problem "?ev[args] = rhs" when "?ev" is * an (uninstantiated) evar such that "hyps |- ?ev : typ". Otherwise said, -- cgit v1.2.3 From 1cd87577ab85a402fb0482678dfcdbe85b45ce38 Mon Sep 17 00:00:00 2001 From: Matthieu Sozeau Date: Tue, 15 Sep 2015 18:33:04 +0200 Subject: Univs: force all universes to be >= Set. --- pretyping/evd.ml | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) (limited to 'pretyping') diff --git a/pretyping/evd.ml b/pretyping/evd.ml index fe5f12dd8a..9f2d284387 100644 --- a/pretyping/evd.ml +++ b/pretyping/evd.ml @@ -385,7 +385,7 @@ let process_universe_constraints univs vars alg cstrs = let levels = Univ.Universe.levels l in Univ.LSet.fold (fun l local -> if Univ.Level.is_small l || Univ.LMap.mem l !vars then - Univ.enforce_eq (Univ.Universe.make l) r local + unify_universes fo (Univ.Universe.make l) Universes.UEq r local else raise (Univ.UniverseInconsistency (Univ.Le, Univ.Universe.make l, r, None))) levels local else @@ -1083,11 +1083,11 @@ let uctx_new_univ_variable rigid name predicative | None -> uctx.uctx_names in let initial = - Univ.add_universe u pred uctx.uctx_initial_universes + Univ.add_universe u true uctx.uctx_initial_universes in let uctx' = {uctx' with uctx_names = names; uctx_local = ctx'; - uctx_universes = Univ.add_universe u pred uctx.uctx_universes; + uctx_universes = Univ.add_universe u true uctx.uctx_universes; uctx_initial_universes = initial} in uctx', u -- cgit v1.2.3 From 4838a3a3c25cc9f7583dd62e4585460aca8ee961 Mon Sep 17 00:00:00 2001 From: Matthieu Sozeau Date: Mon, 21 Sep 2015 11:55:32 +0200 Subject: Forcing i > Set for global universes (incomplete) --- pretyping/evd.ml | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) (limited to 'pretyping') diff --git a/pretyping/evd.ml b/pretyping/evd.ml index 9f2d284387..a25479d483 100644 --- a/pretyping/evd.ml +++ b/pretyping/evd.ml @@ -1083,11 +1083,11 @@ let uctx_new_univ_variable rigid name predicative | None -> uctx.uctx_names in let initial = - Univ.add_universe u true uctx.uctx_initial_universes + Univ.add_universe u false uctx.uctx_initial_universes in let uctx' = {uctx' with uctx_names = names; uctx_local = ctx'; - uctx_universes = Univ.add_universe u true uctx.uctx_universes; + uctx_universes = Univ.add_universe u false uctx.uctx_universes; uctx_initial_universes = initial} in uctx', u -- cgit v1.2.3 From 91f5467917266a85496fb718dfc30eff3565d4dc Mon Sep 17 00:00:00 2001 From: Matthieu Sozeau Date: Wed, 23 Sep 2015 16:20:42 +0200 Subject: Univs (evd): deal with global universes and sideff - Fix union of universe contexts to keep declarations - Fix side-effect handling to register new global universes in the graph. --- pretyping/evd.ml | 137 ++++++++++++++++++++++++++++++++++++------------------ pretyping/evd.mli | 2 + 2 files changed, 95 insertions(+), 44 deletions(-) (limited to 'pretyping') diff --git a/pretyping/evd.ml b/pretyping/evd.ml index a25479d483..8243f96c16 100644 --- a/pretyping/evd.ml +++ b/pretyping/evd.ml @@ -310,6 +310,9 @@ let union_evar_universe_context ctx ctx' = else let local = Univ.ContextSet.union ctx.uctx_local ctx'.uctx_local in let names = UNameMap.union (fst ctx.uctx_names) (fst ctx'.uctx_names) in + let newus = Univ.LSet.diff (Univ.ContextSet.levels ctx'.uctx_local) + (Univ.ContextSet.levels ctx.uctx_local) in + let declarenew g = Univ.LSet.fold (fun u g -> Univ.add_universe u false g) newus g in let names_rev = Univ.LMap.union (snd ctx.uctx_names) (snd ctx'.uctx_names) in { uctx_names = (names, names_rev); uctx_local = local; @@ -317,12 +320,12 @@ let union_evar_universe_context ctx ctx' = Univ.LMap.subst_union ctx.uctx_univ_variables ctx'.uctx_univ_variables; uctx_univ_algebraic = Univ.LSet.union ctx.uctx_univ_algebraic ctx'.uctx_univ_algebraic; - uctx_initial_universes = ctx.uctx_initial_universes; + uctx_initial_universes = declarenew ctx.uctx_initial_universes; uctx_universes = if local == ctx.uctx_local then ctx.uctx_universes else let cstrsr = Univ.ContextSet.constraints ctx'.uctx_local in - Univ.merge_constraints cstrsr ctx.uctx_universes } + Univ.merge_constraints cstrsr (declarenew ctx.uctx_universes) } (* let union_evar_universe_context_key = Profile.declare_profile "union_evar_universe_context";; *) (* let union_evar_universe_context = *) @@ -935,38 +938,6 @@ let evars_of_filtered_evar_info evi = | Evar_defined b -> evars_of_term b) (evars_of_named_context (evar_filtered_context evi))) -(**********************************************************) -(* Side effects *) - -let emit_side_effects eff evd = - { evd with effects = Declareops.union_side_effects eff evd.effects; } - -let drop_side_effects evd = - { evd with effects = Declareops.no_seff; } - -let eval_side_effects evd = evd.effects - -(* Future goals *) -let declare_future_goal evk evd = - { evd with future_goals = evk::evd.future_goals } - -let declare_principal_goal evk evd = - match evd.principal_future_goal with - | None -> { evd with - future_goals = evk::evd.future_goals; - principal_future_goal=Some evk; } - | Some _ -> Errors.error "Only one main subgoal per instantiation." - -let future_goals evd = evd.future_goals - -let principal_future_goal evd = evd.principal_future_goal - -let reset_future_goals evd = - { evd with future_goals = [] ; principal_future_goal=None } - -let restore_future_goals evd gls pgl = - { evd with future_goals = gls ; principal_future_goal = pgl } - (**********************************************************) (* Sort variables *) @@ -1022,13 +993,13 @@ let restrict_universe_context evd vars = let universe_subst evd = evd.universes.uctx_univ_variables -let merge_uctx rigid uctx ctx' = +let merge_uctx sideff rigid uctx ctx' = let open Univ in - let uctx = + let levels = ContextSet.levels ctx' in + let uctx = if sideff then uctx else match rigid with | UnivRigid -> uctx | UnivFlexible b -> - let levels = ContextSet.levels ctx' in let fold u accu = if LMap.mem u accu then accu else LMap.add u None accu @@ -1039,12 +1010,23 @@ let merge_uctx rigid uctx ctx' = uctx_univ_algebraic = LSet.union uctx.uctx_univ_algebraic levels } else { uctx with uctx_univ_variables = uvars' } in - let uctx_local = ContextSet.append ctx' uctx.uctx_local in - let uctx_universes = merge_constraints (ContextSet.constraints ctx') uctx.uctx_universes in - { uctx with uctx_local; uctx_universes } + let uctx_local = + if sideff then uctx.uctx_local + else ContextSet.append ctx' uctx.uctx_local + in + let declare g = + LSet.fold (fun u g -> + try Univ.add_universe u false g + with Univ.AlreadyDeclared when sideff -> g) + levels g + in + let initial = declare uctx.uctx_initial_universes in + let univs = declare uctx.uctx_universes in + let uctx_universes = merge_constraints (ContextSet.constraints ctx') univs in + { uctx with uctx_local; uctx_universes; uctx_initial_universes = initial } let merge_context_set rigid evd ctx' = - {evd with universes = merge_uctx rigid evd.universes ctx'} + {evd with universes = merge_uctx false rigid evd.universes ctx'} let merge_uctx_subst uctx s = { uctx with uctx_univ_variables = Univ.LMap.subst_union uctx.uctx_univ_variables s } @@ -1055,6 +1037,24 @@ let merge_universe_subst evd subst = let with_context_set rigid d (a, ctx) = (merge_context_set rigid d ctx, a) +let emit_universe_side_effects eff u = + Declareops.fold_side_effects + (fun acc eff -> + match eff with + | Declarations.SEscheme (l,s) -> + List.fold_left + (fun acc (_,_,cb,c) -> + let acc = match c with + | `Nothing -> acc + | `Opaque (s, ctx) -> merge_uctx true univ_rigid acc ctx + in if cb.Declarations.const_polymorphic then acc + else + merge_uctx true univ_rigid acc + (Univ.ContextSet.of_context cb.Declarations.const_universes)) + acc l + | Declarations.SEsubproof _ -> acc) + u eff + let add_uctx_names s l (names, names_rev) = (UNameMap.add s l names, Univ.LMap.add l s names_rev) @@ -1103,6 +1103,18 @@ let new_sort_variable ?name ?(predicative=true) rigid d = let (d', u) = new_univ_variable rigid ?name ~predicative d in (d', Type u) +let add_global_univ d u = + let uctx = d.universes in + let initial = + Univ.add_universe u true uctx.uctx_initial_universes + in + let univs = + Univ.add_universe u true uctx.uctx_universes + in + { d with universes = { uctx with uctx_local = Univ.ContextSet.add_universe u uctx.uctx_local; + uctx_initial_universes = initial; + uctx_universes = univs } } + let make_flexible_variable evd b u = let {uctx_univ_variables = uvars; uctx_univ_algebraic = avars} as ctx = evd.universes in let uvars' = Univ.LMap.add u None uvars in @@ -1291,12 +1303,16 @@ let refresh_undefined_univ_variables uctx = Univ.LMap.add (Univ.subst_univs_level_level subst u) (Option.map (Univ.subst_univs_level_universe subst) v) acc) uctx.uctx_univ_variables Univ.LMap.empty - in + in + let declare g = Univ.LSet.fold (fun u g -> Univ.add_universe u false g) + (Univ.ContextSet.levels ctx') g in + let initial = declare uctx.uctx_initial_universes in + let univs = declare Univ.initial_universes in let uctx' = {uctx_names = uctx.uctx_names; uctx_local = ctx'; uctx_univ_variables = vars; uctx_univ_algebraic = alg; - uctx_universes = Univ.initial_universes; - uctx_initial_universes = uctx.uctx_initial_universes } in + uctx_universes = univs; + uctx_initial_universes = initial } in uctx', subst let refresh_undefined_universes evd = @@ -1382,6 +1398,39 @@ let e_eq_constr_univs evdref t u = let evd, b = eq_constr_univs !evdref t u in evdref := evd; b +(**********************************************************) +(* Side effects *) + +let emit_side_effects eff evd = + { evd with effects = Declareops.union_side_effects eff evd.effects; + universes = emit_universe_side_effects eff evd.universes } + +let drop_side_effects evd = + { evd with effects = Declareops.no_seff; } + +let eval_side_effects evd = evd.effects + +(* Future goals *) +let declare_future_goal evk evd = + { evd with future_goals = evk::evd.future_goals } + +let declare_principal_goal evk evd = + match evd.principal_future_goal with + | None -> { evd with + future_goals = evk::evd.future_goals; + principal_future_goal=Some evk; } + | Some _ -> Errors.error "Only one main subgoal per instantiation." + +let future_goals evd = evd.future_goals + +let principal_future_goal evd = evd.principal_future_goal + +let reset_future_goals evd = + { evd with future_goals = [] ; principal_future_goal=None } + +let restore_future_goals evd gls pgl = + { evd with future_goals = gls ; principal_future_goal = pgl } + (**********************************************************) (* Accessing metas *) diff --git a/pretyping/evd.mli b/pretyping/evd.mli index c2ccc6d21a..5a59c1776c 100644 --- a/pretyping/evd.mli +++ b/pretyping/evd.mli @@ -508,6 +508,8 @@ val normalize_evar_universe_context : evar_universe_context -> val new_univ_level_variable : ?name:string -> ?predicative:bool -> rigid -> evar_map -> evar_map * Univ.universe_level val new_univ_variable : ?name:string -> ?predicative:bool -> rigid -> evar_map -> evar_map * Univ.universe val new_sort_variable : ?name:string -> ?predicative:bool -> rigid -> evar_map -> evar_map * sorts +val add_global_univ : evar_map -> Univ.Level.t -> evar_map + val make_flexible_variable : evar_map -> bool -> Univ.universe_level -> evar_map val is_sort_variable : evar_map -> sorts -> Univ.universe_level option (** [is_sort_variable evm s] returns [Some u] or [None] if [s] is -- cgit v1.2.3 From 02aace9f038d579e9cf32dc2f5b21d415e977c03 Mon Sep 17 00:00:00 2001 From: Matthieu Sozeau Date: Wed, 23 Sep 2015 16:23:43 +0200 Subject: Univs (pretyping): allow parsing and decl of Top.n This allows pretyping and detyping to be inverses regarding universes, and makes Function's detyping/pretyping manipulations bearable in presence of global universes that must be declared (otherwise an evd would need to be threaded there in many places as well). --- pretyping/pretyping.ml | 29 +++++++++++++++++++++-------- 1 file changed, 21 insertions(+), 8 deletions(-) (limited to 'pretyping') diff --git a/pretyping/pretyping.ml b/pretyping/pretyping.ml index 2858a5c1fe..edb76e52f4 100644 --- a/pretyping/pretyping.ml +++ b/pretyping/pretyping.ml @@ -102,14 +102,27 @@ let ((constr_in : constr -> Dyn.t), (** Miscellaneous interpretation functions *) let interp_universe_level_name evd s = let names, _ = Universes.global_universe_names () in - try - let id = try Id.of_string s with _ -> raise Not_found in - evd, Idmap.find id names - with Not_found -> - try let level = Evd.universe_of_name evd s in - evd, level - with Not_found -> - new_univ_level_variable ~name:s univ_rigid evd + if CString.string_contains s "." then + match List.rev (CString.split '.' s) with + | [] -> anomaly (str"Invalid universe name " ++ str s) + | n :: dp -> + let num = int_of_string n in + let dp = DirPath.make (List.map Id.of_string dp) in + let level = Univ.Level.make dp num in + let evd = + try Evd.add_global_univ evd level + with Univ.AlreadyDeclared -> evd + in evd, level + else + try + let id = + try Id.of_string s with _ -> raise Not_found in + evd, Idmap.find id names + with Not_found -> + try let level = Evd.universe_of_name evd s in + evd, level + with Not_found -> + new_univ_level_variable ~name:s univ_rigid evd let interp_universe evd = function | [] -> let evd, l = new_univ_level_variable univ_rigid evd in -- cgit v1.2.3 From 91b1808056602f3e26d1eb1bdf7be1e791cb742d Mon Sep 17 00:00:00 2001 From: Matthieu Sozeau Date: Wed, 23 Sep 2015 16:35:07 +0200 Subject: Univs: fix many evar_map initializations and leaks. --- pretyping/typeclasses.ml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'pretyping') diff --git a/pretyping/typeclasses.ml b/pretyping/typeclasses.ml index 18e83056bd..2ef2896506 100644 --- a/pretyping/typeclasses.ml +++ b/pretyping/typeclasses.ml @@ -370,7 +370,7 @@ let add_instance check inst = List.iter (fun (path, pri, c) -> add_instance_hint (IsConstr c) path (is_local inst) pri poly) (build_subclasses ~check:(check && not (isVarRef inst.is_impl)) - (Global.env ()) Evd.empty inst.is_impl inst.is_pri) + (Global.env ()) (Evd.from_env (Global.env ())) inst.is_impl inst.is_pri) let rebuild_instance (action, inst) = let () = match action with -- cgit v1.2.3 From c92946243ccb0b11cd138f040a5297979229c3f5 Mon Sep 17 00:00:00 2001 From: Matthieu Sozeau Date: Wed, 23 Sep 2015 19:01:31 +0200 Subject: Univs: fix after rebase (from_ctx/from_env) --- pretyping/evd.ml | 7 ++++--- 1 file changed, 4 insertions(+), 3 deletions(-) (limited to 'pretyping') diff --git a/pretyping/evd.ml b/pretyping/evd.ml index 8243f96c16..842b87c57e 100644 --- a/pretyping/evd.ml +++ b/pretyping/evd.ml @@ -1136,9 +1136,10 @@ let make_evar_universe_context e l = match l with | None -> uctx | Some us -> - List.fold_left (fun uctx (loc,id) -> - fst (uctx_new_univ_variable univ_rigid (Some (Id.to_string id)) uctx)) - uctx us + List.fold_left + (fun uctx (loc,id) -> + fst (uctx_new_univ_variable univ_rigid (Some (Id.to_string id)) true uctx)) + uctx us (****************************************) (* Operations on constants *) -- cgit v1.2.3 From b3d97c2147418f44fc704807d3812b04921591af Mon Sep 17 00:00:00 2001 From: Matthieu Sozeau Date: Thu, 1 Oct 2015 15:36:57 +0200 Subject: Univs: fix bug #4251, handling of template polymorphic constants. --- pretyping/pretyping.ml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'pretyping') diff --git a/pretyping/pretyping.ml b/pretyping/pretyping.ml index edb76e52f4..f18657da82 100644 --- a/pretyping/pretyping.ml +++ b/pretyping/pretyping.ml @@ -645,7 +645,7 @@ let rec pretype k0 resolve_tc (tycon : type_constraint) env evdref (lvar : ltac_ match evar_kind_of_term !evdref resj.uj_val with | App (f,args) -> let f = whd_evar !evdref f in - if isInd f && is_template_polymorphic env f then + if is_template_polymorphic env f then (* Special case for inductive type applications that must be refreshed right away. *) let sigma = !evdref in -- cgit v1.2.3