diff options
Diffstat (limited to 'tactics/decl_proof_instr.ml')
| -rw-r--r-- | tactics/decl_proof_instr.ml | 6 |
1 files changed, 3 insertions, 3 deletions
diff --git a/tactics/decl_proof_instr.ml b/tactics/decl_proof_instr.ml index 839a494a..2d0395a3 100644 --- a/tactics/decl_proof_instr.ml +++ b/tactics/decl_proof_instr.ml @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id: decl_proof_instr.ml 11671 2008-12-12 12:43:03Z herbelin $ *) +(* $Id: decl_proof_instr.ml 11897 2009-02-09 19:28:02Z barras $ *) open Util open Pp @@ -1093,7 +1093,7 @@ let thesis_for obj typ per_info env= ((Printer.pr_constr_env env obj) ++ spc () ++ str "cannot give an induction hypothesis (wrong parameters).") in let hd2 = (applist ((lift (List.length rc) per_info.per_pred),args@[obj])) in - compose_prod rc (whd_beta hd2) + compose_prod rc (whd_beta Evd.empty hd2) let rec build_product_dep pat_info per_info args body gls = match args with @@ -1225,7 +1225,7 @@ let hrec_for fix_id per_info gls obj_id = try List.for_all2 eq_constr params per_info.per_params with Invalid_argument _ -> false end; let hd2 = applist (mkVar fix_id,args@[obj]) in - compose_lam rc (whd_beta hd2) + compose_lam rc (whd_beta gls.sigma hd2) let rec execute_cases fix_name per_info tacnext args objs nhrec tree gls = match tree, objs with |