diff options
| author | Pierre-Marie Pédrot | 2016-11-25 18:34:53 +0100 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2017-02-14 17:30:41 +0100 |
| commit | 02dd160233adc784eac732d97a88356d1f0eaf9b (patch) | |
| tree | d2baacdc2a4ae06e4607bfe09b48ba2c23a78a0f /plugins/funind/indfun.ml | |
| parent | a5499688bd76def8de3d8e1089a49c7a08430903 (diff) | |
Removing various compatibility layers of tactics.
Diffstat (limited to 'plugins/funind/indfun.ml')
| -rw-r--r-- | plugins/funind/indfun.ml | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/plugins/funind/indfun.ml b/plugins/funind/indfun.ml index e22fed391e..1cde4420e5 100644 --- a/plugins/funind/indfun.ml +++ b/plugins/funind/indfun.ml @@ -78,11 +78,11 @@ let functional_induction with_clean c princl pat = ++Printer.pr_leconstr (mkConst c') ) in let princ = EConstr.of_constr princ in - (princ,NoBindings,EConstr.of_constr (Tacmach.pf_unsafe_type_of g' princ),g') + (princ,NoBindings,Tacmach.pf_unsafe_type_of g' princ,g') | _ -> raise (UserError(None,str "functional induction must be used with a function" )) end | Some ((princ,binding)) -> - princ,binding,EConstr.of_constr (Tacmach.pf_unsafe_type_of g princ),g + princ,binding,Tacmach.pf_unsafe_type_of g princ,g in let sigma = Tacmach.project g' in let princ_infos = Tactics.compute_elim_sig (Tacmach.project g') princ_type in |