diff options
Diffstat (limited to 'tactics/equality.ml')
| -rw-r--r-- | tactics/equality.ml | 6 |
1 files changed, 3 insertions, 3 deletions
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 |