diff options
| author |  jforest <jforest@daneel.lan.home> | 2015-03-25 10:27:13 +0100 |
|---|---|---|
| committer | jforest <jforest@daneel.lan.home> | 2015-03-25 10:27:53 +0100 |
| commit | f54d0b3158bc69a11fe579289f06f164ff5ccb94 (patch) | |
| tree | 2f180794423d49595cc2e9eee54a0fa7d71a7366 | |
| parent | 810454922d4eeffaf9f92ccd7d8e10a1433de947 (diff) | |
Correcting a bug introduced by universes polymorphism
| -rw-r--r-- | plugins/funind/functional_principles_types.ml | 5 |
1 files changed, 3 insertions, 2 deletions
diff --git a/plugins/funind/functional_principles_types.ml b/plugins/funind/functional_principles_types.ml index d4f49af4d..deaf603ef 100644 --- a/plugins/funind/functional_principles_types.ml +++ b/plugins/funind/functional_principles_types.ml @@ -274,10 +274,11 @@ let build_functional_principle interactive_proof old_princ_type sorts funs i pro in let hook = Lemmas.mk_hook (hook new_principle_type) in begin + let evd,_ = Typing.e_type_of ~refresh:true (Global.env ()) Evd.empty new_principle_type in Lemmas.start_proof new_princ_name (Decl_kinds.Global,false,(Decl_kinds.Proof Decl_kinds.Theorem)) - (*FIXME*) Evd.empty + evd new_principle_type hook ; @@ -323,7 +324,7 @@ let generate_functional_principle let name = Indrec.make_elimination_ident base_new_princ_name fam_sort in let value = change_property_sort s new_principle_type new_princ_name in (* Pp.msgnl (str "new principle := " ++ pr_lconstr value); *) - let ce = Declare.definition_entry value in (*FIXME, no poly, nothing *) + let ce = Declare.definition_entry value in ignore( Declare.declare_constant name |