diff options
author | Matthieu Sozeau <mattam@mattam.org> | 2013-10-17 14:55:57 +0200 |
---|---|---|
committer | Matthieu Sozeau <mattam@mattam.org> | 2014-05-06 09:58:53 +0200 |
commit | 84cbc09bd1400f732a6c70e8a840e4c13d018478 (patch) | |
tree | f6b3417e653bea9de8f0d8f510ad19ccdbb4840e /pretyping/program.ml | |
parent | 57bee17f928fc67a599d2116edb42a59eeb21477 (diff) |
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.
-
Diffstat (limited to 'pretyping/program.ml')
-rw-r--r-- | pretyping/program.ml | 36 |
1 files changed, 20 insertions, 16 deletions
diff --git a/pretyping/program.ml b/pretyping/program.ml index 67bb3bd2a..a0ecfb1f9 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" |