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. - --- pretyping/program.ml | 36 ++++++++++++++++++++---------------- 1 file changed, 20 insertions(+), 16 deletions(-) (limited to 'pretyping/program.ml') diff --git a/pretyping/program.ml b/pretyping/program.ml index 67bb3bd2a7..a0ecfb1f92 100644 --- a/pretyping/program.ml +++ b/pretyping/program.ml @@ -26,27 +26,31 @@ let coq_constant locstr dir s = Universes.constr_of_global (coq_reference locstr let init_constant dir s () = coq_constant "Program" dir s let init_reference dir s () = coq_reference "Program" dir s -let sig_typ = init_constant ["Init"; "Specif"] "sig" -let sig_intro = init_constant ["Init"; "Specif"] "exist" -let sig_proj1 = init_constant ["Init"; "Specif"] "proj1_sig" +let papp evdref r args = + let gr = delayed_force r in + mkApp (Evarutil.e_new_global evdref gr, args) -let sigT_typ = init_constant ["Init"; "Specif"] "sigT" -let sigT_intro = init_constant ["Init"; "Specif"] "existT" -let sigT_proj1 = init_constant ["Init"; "Specif"] "projT1" -let sigT_proj2 = init_constant ["Init"; "Specif"] "projT2" +let sig_typ = init_reference ["Init"; "Specif"] "sig" +let sig_intro = init_reference ["Init"; "Specif"] "exist" +let sig_proj1 = init_reference ["Init"; "Specif"] "proj1_sig" -let prod_typ = init_constant ["Init"; "Datatypes"] "prod" -let prod_intro = init_constant ["Init"; "Datatypes"] "pair" -let prod_proj1 = init_constant ["Init"; "Datatypes"] "fst" -let prod_proj2 = init_constant ["Init"; "Datatypes"] "snd" +let sigT_typ = init_reference ["Init"; "Specif"] "sigT" +let sigT_intro = init_reference ["Init"; "Specif"] "existT" +let sigT_proj1 = init_reference ["Init"; "Specif"] "projT1" +let sigT_proj2 = init_reference ["Init"; "Specif"] "projT2" -let coq_eq_ind = init_constant ["Init"; "Logic"] "eq" -let coq_eq_refl = init_constant ["Init"; "Logic"] "eq_refl" +let prod_typ = init_reference ["Init"; "Datatypes"] "prod" +let prod_intro = init_reference ["Init"; "Datatypes"] "pair" +let prod_proj1 = init_reference ["Init"; "Datatypes"] "fst" +let prod_proj2 = init_reference ["Init"; "Datatypes"] "snd" + +let coq_eq_ind = init_reference ["Init"; "Logic"] "eq" +let coq_eq_refl = init_reference ["Init"; "Logic"] "eq_refl" let coq_eq_refl_ref = init_reference ["Init"; "Logic"] "eq_refl" -let coq_eq_rect = init_constant ["Init"; "Logic"] "eq_rect" +let coq_eq_rect = init_reference ["Init"; "Logic"] "eq_rect" -let coq_JMeq_ind = init_constant ["Logic";"JMeq"] "JMeq" -let coq_JMeq_refl = init_constant ["Logic";"JMeq"] "JMeq_refl" +let coq_JMeq_ind = init_reference ["Logic";"JMeq"] "JMeq" +let coq_JMeq_refl = init_reference ["Logic";"JMeq"] "JMeq_refl" let coq_not = init_constant ["Init";"Logic"] "not" let coq_and = init_constant ["Init";"Logic"] "and" -- cgit v1.2.3