diff options
Diffstat (limited to 'plugins/funind')
| -rw-r--r-- | plugins/funind/functional_principles_types.ml | 8 | ||||
| -rw-r--r-- | plugins/funind/invfun.ml | 17 | ||||
| -rw-r--r-- | plugins/funind/recdef.ml | 15 |
3 files changed, 15 insertions, 25 deletions
diff --git a/plugins/funind/functional_principles_types.ml b/plugins/funind/functional_principles_types.ml index f70ce00924..efed9a8560 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 } ) diff --git a/plugins/funind/invfun.ml b/plugins/funind/invfun.ml index fd074386ec..7d14d1408c 100644 --- a/plugins/funind/invfun.ml +++ b/plugins/funind/invfun.ml @@ -1013,10 +1013,9 @@ let do_save () = Lemmas.save_named false *) let derive_correctness make_scheme functional_induction (funs: constant list) (graphs:inductive list) = - let previous_state = States.freeze ~marshallable:false in let funs = Array.of_list funs and graphs = Array.of_list graphs in let funs_constr = Array.map mkConst funs in - try + States.with_state_protection (fun () -> let graphs_constr = Array.map mkInd graphs in let lemmas_types_infos = Util.Array.map2_i @@ -1044,7 +1043,7 @@ let derive_correctness make_scheme functional_induction (funs: constant list) (g Array.of_list (List.map (fun entry -> - (entry.Entries.const_entry_body, Option.get entry.Entries.const_entry_type ) + (fst(Future.force entry.Entries.const_entry_body), Option.get entry.Entries.const_entry_type ) ) (make_scheme (Array.map_to_list (fun const -> const,GType None) funs)) ) @@ -1122,16 +1121,8 @@ let derive_correctness make_scheme functional_induction (funs: constant list) (g let lem_cst = destConst (Constrintern.global_reference lem_id) in update_Function {finfo with completeness_lemma = Some lem_cst} ) - funs; - with reraise -> - (* In case of problem, we reset all the lemmas *) - Pfedit.delete_all_proofs (); - States.unfreeze previous_state; - raise reraise - - - - + funs) + () (***********************************************) diff --git a/plugins/funind/recdef.ml b/plugins/funind/recdef.ml index 4b9704c2c9..68b291ff96 100644 --- a/plugins/funind/recdef.ml +++ b/plugins/funind/recdef.ml @@ -57,7 +57,8 @@ let find_reference sl s = let (declare_fun : Id.t -> logical_kind -> constr -> global_reference) = fun f_id kind value -> - let ce = {const_entry_body = value; + let ce = {const_entry_body = Future.from_val + (value, Declareops.no_seff); const_entry_secctx = None; const_entry_type = None; const_entry_opaque = false; @@ -1261,7 +1262,7 @@ let open_new_goal (build_proof:tactic -> tactic -> unit) using_lemmas ref_ goal_ ref_ := Some lemma ; let lid = ref [] in let h_num = ref (-1) in - ignore (Flags.silently Vernacentries.interp (Vernacexpr.VernacAbort None)); + ignore (Flags.silently Vernacentries.interp (Loc.ghost,Vernacexpr.VernacAbort None)); build_proof ( fun gls -> let hid = next_ident_away_in_goal h_id (pf_ids_of_hyps gls) in @@ -1443,7 +1444,6 @@ let (com_eqn : int -> Id.t -> let recursive_definition is_mes function_name rec_impls type_of_f r rec_arg_num eq generate_induction_principle using_lemmas : unit = - let previous_label = Lib.current_command_label () in let function_type = interp_constr Evd.empty (Global.env()) type_of_f in let env = push_named (function_name,None,function_type) (Global.env()) in (* Pp.msgnl (str "function type := " ++ Printer.pr_lconstr function_type); *) @@ -1513,7 +1513,7 @@ let recursive_definition is_mes function_name rec_impls type_of_f r rec_arg_num spc () ++ str"is defined" ) ) in - try + States.with_state_protection (fun () -> com_terminate tcc_lemma_name tcc_lemma_constr @@ -1523,9 +1523,6 @@ let recursive_definition is_mes function_name rec_impls type_of_f r rec_arg_num term_id using_lemmas (List.length res_vars) - hook - with reraise -> - ignore (Backtrack.backto previous_label); - (* anomaly (Pp.str "Cannot create termination Lemma") *) - raise reraise + hook) + () |