diff options
Diffstat (limited to 'tactics')
| -rw-r--r-- | tactics/class_tactics.ml4 | 8 | ||||
| -rw-r--r-- | tactics/decl_proof_instr.ml | 6 | ||||
| -rw-r--r-- | tactics/equality.ml | 6 | ||||
| -rw-r--r-- | tactics/leminv.ml | 5 | ||||
| -rw-r--r-- | tactics/tactics.ml | 9 |
5 files changed, 18 insertions, 16 deletions
diff --git a/tactics/class_tactics.ml4 b/tactics/class_tactics.ml4 index e609fb77..6a425984 100644 --- a/tactics/class_tactics.ml4 +++ b/tactics/class_tactics.ml4 @@ -9,7 +9,7 @@ (*i camlp4deps: "parsing/grammar.cma" i*) -(* $Id: class_tactics.ml4 11823 2009-01-21 15:32:37Z msozeau $ *) +(* $Id: class_tactics.ml4 11897 2009-02-09 19:28:02Z barras $ *) open Pp open Util @@ -650,14 +650,14 @@ let build_signature isevars env m (cstrs : 'a option list) (finalcstr : 'a Lazy. | Prod (na, ty, b), obj :: cstrs -> if dependent (mkRel 1) b then let (b, arg, evars) = aux (Environ.push_rel (na, None, ty) env) b cstrs in - let ty = Reductionops.nf_betaiota ty in + let ty = Reductionops.nf_betaiota (Evd.evars_of !isevars) ty in let pred = mkLambda (na, ty, b) in let liftarg = mkLambda (na, ty, arg) in let arg' = mkApp (Lazy.force forall_relation, [| ty ; pred ; liftarg |]) in mkProd(na, ty, b), arg', (ty, None) :: evars else let (b', arg, evars) = aux env (subst1 mkProp b) cstrs in - let ty = Reductionops.nf_betaiota ty in + let ty = Reductionops.nf_betaiota(Evd.evars_of !isevars) ty in let relty = mk_relty ty obj in let newarg = mkApp (Lazy.force respectful, [| ty ; b' ; relty ; arg |]) in mkProd(na, ty, b), newarg, (ty, Some relty) :: evars @@ -665,7 +665,7 @@ let build_signature isevars env m (cstrs : 'a option list) (finalcstr : 'a Lazy. | _, [] -> (match finalcstr with None -> - let t = Reductionops.nf_betaiota ty in + let t = Reductionops.nf_betaiota(Evd.evars_of !isevars) ty in let rel = mk_relty t None in t, rel, [t, Some rel] | Some codom -> let (t, rel) = Lazy.force codom in 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 diff --git a/tactics/equality.ml b/tactics/equality.ml index ba18430a..baebee07 100644 --- a/tactics/equality.ml +++ b/tactics/equality.ml @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id: equality.ml 11800 2009-01-18 18:34:15Z msozeau $ *) +(* $Id: equality.ml 11897 2009-02-09 19:28:02Z barras $ *) open Pp open Util @@ -120,7 +120,7 @@ let general_rewrite_ebindings_clause cls lft2rgt occs ((c,l) : open_constr with_ let sigma, c' = c in let sigma = Evd.merge sigma (project gl) in let ctype = get_type_of env sigma c' in - let rels, t = decompose_prod (whd_betaiotazeta ctype) in + let rels, t = decompose_prod (whd_betaiotazeta sigma ctype) in match match_with_equality_type t with | Some (hdcncl,args) -> (* Fast path: direct leibniz rewrite *) let lft2rgt = adjust_rewriting_direction args lft2rgt in @@ -737,7 +737,7 @@ let sig_clausal_form env sigma sort_of_ty siglen ty dflt = else error "Cannot solve an unification problem." else - let (a,p_i_minus_1) = match whd_beta_stack p_i with + let (a,p_i_minus_1) = match whd_beta_stack (evars_of !evdref) p_i with | (_sigS,[a;p]) -> (a,p) | _ -> anomaly "sig_clausal_form: should be a sigma type" in let ev = Evarutil.e_new_evar evdref env a in diff --git a/tactics/leminv.ml b/tactics/leminv.ml index 5acc5197..e798f59a 100644 --- a/tactics/leminv.ml +++ b/tactics/leminv.ml @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id: leminv.ml 11309 2008-08-06 10:30:35Z herbelin $ *) +(* $Id: leminv.ml 11897 2009-02-09 19:28:02Z barras $ *) open Pp open Util @@ -237,7 +237,8 @@ let inversion_scheme env sigma t sort dep_option inv_op = meta_types in let invProof = - it_mkNamedLambda_or_LetIn (local_strong (whd_meta mvb) pfterm) ownSign + it_mkNamedLambda_or_LetIn + (local_strong (fun _ -> whd_meta mvb) Evd.empty pfterm) ownSign in invProof diff --git a/tactics/tactics.ml b/tactics/tactics.ml index 5af5c0d5..2c567034 100644 --- a/tactics/tactics.ml +++ b/tactics/tactics.ml @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id: tactics.ml 11745 2009-01-04 18:43:08Z herbelin $ *) +(* $Id: tactics.ml 11897 2009-02-09 19:28:02Z barras $ *) open Pp open Util @@ -759,7 +759,7 @@ let general_apply with_delta with_destruct with_evars (c,lbind) gl0 = let concl_nprod = nb_prod (pf_concl gl0) in let evm, c = c in let rec try_main_apply c gl = - let thm_ty0 = nf_betaiota (pf_type_of gl c) in + let thm_ty0 = nf_betaiota (project gl) (pf_type_of gl c) in let try_apply thm_ty nprod = let n = nb_prod thm_ty - nprod in if n<0 then error "Applied theorem has not enough premisses."; @@ -850,7 +850,7 @@ let progress_with_clause flags innerclause clause = with Failure _ -> error "Unable to unify." let apply_in_once_main flags innerclause (d,lbind) gl = - let thm = nf_betaiota (pf_type_of gl d) in + let thm = nf_betaiota gl.sigma (pf_type_of gl d) in let rec aux clause = try progress_with_clause flags innerclause clause with err -> @@ -985,7 +985,8 @@ let specialize mopt (c,lbind) g = else let clause = make_clenv_binding g (c,pf_type_of g c) lbind in let clause = clenv_unify_meta_types clause in - let (thd,tstack) = whd_stack (clenv_value clause) in + let (thd,tstack) = + whd_stack (evars_of clause.evd) (clenv_value clause) in let nargs = List.length tstack in let tstack = match mopt with | Some m -> |