From 84cbc09bd1400f732a6c70e8a840e4c13d018478 Mon Sep 17 00:00:00 2001 From: Matthieu Sozeau Date: Thu, 17 Oct 2013 14:55:57 +0200 Subject: Correct rebase on STM code. Thanks to E. Tassi for help on dealing with latent universes. Now the universes in the type of a definition/lemma are eagerly added to the environment so that later proofs can be checked independently of the original (delegated) proof body. - Fixed firstorder, ring to work correctly with universe polymorphism. - Changed constr_of_global to raise an anomaly if side effects would be lost by turning a polymorphic constant into a constr. - Fix a non-termination issue in solve_evar_evar. - --- plugins/funind/recdef.ml | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) (limited to 'plugins/funind/recdef.ml') diff --git a/plugins/funind/recdef.ml b/plugins/funind/recdef.ml index 96bf4c921..50e7507f4 100644 --- a/plugins/funind/recdef.ml +++ b/plugins/funind/recdef.ml @@ -75,7 +75,7 @@ let type_of_const t = Const sp -> Typeops.type_of_constant (Global.env()) sp |_ -> assert false -let constr_of_global = Universes.constr_of_global +let constr_of_global = Universes.unsafe_constr_of_global let constant sl s = constr_of_global (find_reference sl s) @@ -1016,7 +1016,7 @@ let compute_terminate_type nb_args func = delayed_force nat, (mkProd (Name k_id, delayed_force nat, mkArrow cond result))))|])in - let value = mkApp(delayed_force coq_sig, + let value = mkApp(constr_of_global (delayed_force coq_sig_ref), [|b; (mkLambda (Name v_id, b, nb_iter))|]) in compose_prod rev_args value -- cgit v1.2.3