diff options
Diffstat (limited to 'plugins/funind/functional_principles_types.ml')
| -rw-r--r-- | plugins/funind/functional_principles_types.ml | 8 |
1 files changed, 5 insertions, 3 deletions
diff --git a/plugins/funind/functional_principles_types.ml b/plugins/funind/functional_principles_types.ml index f70ce0092..efed9a856 100644 --- a/plugins/funind/functional_principles_types.ml +++ b/plugins/funind/functional_principles_types.ml @@ -339,7 +339,8 @@ let generate_functional_principle let value = change_property_sort s new_principle_type new_princ_name in (* Pp.msgnl (str "new principle := " ++ pr_lconstr value); *) let ce = - { const_entry_body = value; + { const_entry_body = + Future.from_val (value,Declareops.no_seff); const_entry_secctx = None; const_entry_type = None; const_entry_opaque = false; @@ -556,7 +557,7 @@ let make_scheme (fas : (constant*glob_sort) list) : Entries.definition_entry lis List.map (compute_new_princ_type_from_rel funs sorts) other_princ_types in let first_princ_body,first_princ_type = const.Entries.const_entry_body, const.Entries.const_entry_type in - let ctxt,fix = decompose_lam_assum first_princ_body in (* the principle has for forall ...., fix .*) + let ctxt,fix = decompose_lam_assum (fst(Future.force first_princ_body)) in (* the principle has for forall ...., fix .*) let (idxs,_),(_,ta,_ as decl) = destFix fix in let other_result = List.map (* we can now compute the other principles *) @@ -598,7 +599,8 @@ let make_scheme (fas : (constant*glob_sort) list) : Entries.definition_entry lis Termops.it_mkLambda_or_LetIn (mkFix((idxs,i),decl)) ctxt in {const with - Entries.const_entry_body = princ_body; + Entries.const_entry_body = + (Future.from_val (princ_body,Declareops.no_seff)); Entries.const_entry_type = Some scheme_type } ) |