diff options
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" |