From 043c3907f9ed23ae9b9642d2cbb651f6a29737bd Mon Sep 17 00:00:00 2001 From: Julien Forest Date: Fri, 31 Mar 2017 19:48:03 +0200 Subject: Solving first problem in bug #4306. TO DO : solve the let in problem --- plugins/funind/functional_principles_proofs.ml | 11 ++++++----- 1 file changed, 6 insertions(+), 5 deletions(-) (limited to 'plugins/funind/functional_principles_proofs.ml') diff --git a/plugins/funind/functional_principles_proofs.ml b/plugins/funind/functional_principles_proofs.ml index 0bbe4bb4cb..85084badd5 100644 --- a/plugins/funind/functional_principles_proofs.ml +++ b/plugins/funind/functional_principles_proofs.ml @@ -1388,8 +1388,8 @@ let prove_princ_for_struct (evd:Evd.evar_map ref) interactive_proof fun_num fnam let prove_with_tcc tcc_lemma_constr eqs : tactic = match !tcc_lemma_constr with - | None -> anomaly (Pp.str "No tcc proof !!") - | Some lemma -> + | Undefined -> anomaly (Pp.str "No tcc proof !!") + | Value lemma -> fun gls -> (* let hid = next_ident_away_in_goal h_id (pf_ids_of_hyps gls) in *) (* let ids = hid::pf_ids_of_hyps gls in *) @@ -1407,7 +1407,7 @@ let prove_with_tcc tcc_lemma_constr eqs : tactic = Proofview.V82.of_tactic (Eauto.gen_eauto (false,5) [] (Some [])) ] gls - + | Not_needed -> tclIDTAC let backtrack_eqs_until_hrec hrec eqs : tactic = fun gls -> @@ -1586,8 +1586,9 @@ let prove_principle_for_gen let args_ids = List.map (fun decl -> Nameops.out_name (get_name decl)) princ_info.args in let lemma = match !tcc_lemma_ref with - | None -> error "No tcc proof !!" - | Some lemma -> lemma + | Undefined -> error "No tcc proof !!" + | Value lemma -> lemma + | Not_needed -> Coqlib.build_coq_True () in (* let rec list_diff del_list check_list = *) (* match del_list with *) -- cgit v1.2.3 From edface9ff8462a8ecbffd03074e51f589861d88a Mon Sep 17 00:00:00 2001 From: Julien Forest Date: Fri, 31 Mar 2017 21:12:17 +0200 Subject: Bad correction in previous commit --- plugins/funind/functional_principles_proofs.ml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'plugins/funind/functional_principles_proofs.ml') diff --git a/plugins/funind/functional_principles_proofs.ml b/plugins/funind/functional_principles_proofs.ml index 85084badd5..d6a67219ff 100644 --- a/plugins/funind/functional_principles_proofs.ml +++ b/plugins/funind/functional_principles_proofs.ml @@ -1588,7 +1588,7 @@ let prove_principle_for_gen match !tcc_lemma_ref with | Undefined -> error "No tcc proof !!" | Value lemma -> lemma - | Not_needed -> Coqlib.build_coq_True () + | Not_needed -> Coqlib.build_coq_I () in (* let rec list_diff del_list check_list = *) (* match del_list with *) -- cgit v1.2.3 From e242bab34b0b74bc1a02eaf750056d2684d72c36 Mon Sep 17 00:00:00 2001 From: Julien Forest Date: Tue, 4 Apr 2017 13:43:11 +0200 Subject: end of correction of bug 4306 --- plugins/funind/functional_principles_proofs.ml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'plugins/funind/functional_principles_proofs.ml') diff --git a/plugins/funind/functional_principles_proofs.ml b/plugins/funind/functional_principles_proofs.ml index d6a67219ff..a380443fe3 100644 --- a/plugins/funind/functional_principles_proofs.ml +++ b/plugins/funind/functional_principles_proofs.ml @@ -291,7 +291,7 @@ let change_eq env sigma hyp_id (context:Context.Rel.t) x t end_of_type = Can be safely replaced by the next comment for Ocaml >= 3.08.4 *) let sub = Int.Map.bindings sub in - List.fold_left (fun end_of_type (i,t) -> lift 1 (substnl [t] (i-1) end_of_type)) + List.fold_left (fun end_of_type (i,t) -> liftn 1 i (substnl [t] (i-1) end_of_type)) end_of_type_with_pop sub in -- cgit v1.2.3