diff options
| author | Maxime Dénès | 2017-04-19 09:18:31 +0200 |
|---|---|---|
| committer | Maxime Dénès | 2017-04-19 09:18:31 +0200 |
| commit | 59b0041147a9d2dddc1fe14f624a2cf5695f2ea2 (patch) | |
| tree | d4967d23e54ea5162b0dfb8670857bba3f9360c2 /plugins/funind/functional_principles_proofs.ml | |
| parent | 727ef1bd345f9ad9e08d9e4f136e2db7d034a93d (diff) | |
| parent | 031d0fbcea7c1390dc7e6cf89cfaee8609ecfed1 (diff) | |
Merge PR#538: Correction of bug #4306
Diffstat (limited to 'plugins/funind/functional_principles_proofs.ml')
| -rw-r--r-- | plugins/funind/functional_principles_proofs.ml | 13 |
1 files changed, 7 insertions, 6 deletions
diff --git a/plugins/funind/functional_principles_proofs.ml b/plugins/funind/functional_principles_proofs.ml index 0bbe4bb4cb..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 @@ -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_I () in (* let rec list_diff del_list check_list = *) (* match del_list with *) |