diff options
| author |  herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2010-06-29 08:27:03 +0000 |
|---|---|---|
| committer | herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2010-06-29 08:27:03 +0000 |
| commit | 7e2f953c3c19904616c43990fada92e762aadec9 (patch) | |
| tree | 8268d6e2b66ccdcce69df129ed98703e87f141b0 /tactics/rewrite.ml4 | |
| parent | ee711f8994d5e2e94cc61292ac6aab125c23df1c (diff) | |
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
Diffstat (limited to 'tactics/rewrite.ml4')
| -rw-r--r-- | tactics/rewrite.ml4 | 8 |
1 files changed, 4 insertions, 4 deletions
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 = |