From 7e2f953c3c19904616c43990fada92e762aadec9 Mon Sep 17 00:00:00 2001 From: herbelin Date: Tue, 29 Jun 2010 08:27:03 +0000 Subject: Made tclABSTRACT normalize evars before saying it does not support them. This was the cause of the failure of compilation of CyclicAxioms after "replace" starting supporting open constrs (r13206). Seized the opportunity to clean a little bit things around nf_evar, whd_evar, check_evars, etc. Removed obsolete printer mod_self_id from dev/db. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13214 85f007b7-540e-0410-9357-904b9bb8a0f7 --- tactics/rewrite.ml4 | 8 ++++---- 1 file changed, 4 insertions(+), 4 deletions(-) (limited to 'tactics/rewrite.ml4') diff --git a/tactics/rewrite.ml4 b/tactics/rewrite.ml4 index 12a14eb01..a0d0027e4 100644 --- a/tactics/rewrite.ml4 +++ b/tactics/rewrite.ml4 @@ -1006,12 +1006,12 @@ let cl_rewrite_clause_aux ?(abs=None) strat goal_meta clause gl = let cstrevars = !evars in let evars = solve_constraints env cstrevars in let p = map_rewprf - (fun p -> nf_zeta env evars (Evarutil.nf_isevar evars p)) + (fun p -> nf_zeta env evars (Evarutil.nf_evar evars p)) p in - let newt = Evarutil.nf_isevar evars newt in + let newt = Evarutil.nf_evar evars newt in let abs = Option.map (fun (x, y) -> - Evarutil.nf_isevar evars x, Evarutil.nf_isevar evars y) abs in + Evarutil.nf_evar evars x, Evarutil.nf_evar evars y) abs in let undef = split_evars (fst cstrevars) evars in let rewtac = match is_hyp with @@ -1422,7 +1422,7 @@ let build_morphism_signature m = mkApp (Lazy.force proper_type, [| t; sig_; m |]) in let evd = solve_constraints env !isevars in - let m = Evarutil.nf_isevar evd morph in + let m = Evarutil.nf_evar evd morph in Evarutil.check_evars env Evd.empty evd m; m let default_morphism sign m = -- cgit v1.2.3