diff options
| author | msozeau | 2008-03-18 11:22:13 +0000 |
|---|---|---|
| committer | msozeau | 2008-03-18 11:22:13 +0000 |
| commit | d4685a5bdaf15c31ddc616777b05280ec7570d08 (patch) | |
| tree | 1349f628eb8cb3dcfbaf9d5d78bce185f10a8f39 /tactics | |
| parent | 99541c1123793d1c6352d1326c40426024b55948 (diff) | |
Correct implementation of normalization of signatures using setoid
rewriting, in some sense bootstrapping the system. Remove redundant
morphisms for now to test for completeness (small performance penalty).
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10689 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'tactics')
| -rw-r--r-- | tactics/class_tactics.ml4 | 6 |
1 files changed, 2 insertions, 4 deletions
diff --git a/tactics/class_tactics.ml4 b/tactics/class_tactics.ml4 index 998e767f53..b2684a3928 100644 --- a/tactics/class_tactics.ml4 +++ b/tactics/class_tactics.ml4 @@ -824,8 +824,8 @@ let cl_rewrite_clause_aux hypinfo goal_meta occs clause gl = if not (evd = Evd.empty) then Refiner.tclEVARS (Evd.merge sigma evd) else tclIDTAC in tclTHENLIST [evartac; rewtac] gl - with UserError (env, e) -> - tclFAIL 0 (str" setoid rewrite failed: unable to satisfy the rewriting constraints") gl) + with UserError (s, pp) -> + tclFAIL 0 (str" setoid rewrite failed: unable to satisfy the rewriting constraints:" ++ fnl () ++ pp) gl) | None -> let {l2r=l2r; c1=x; c2=y} = !hypinfo in raise (Pretype_errors.PretypeError (pf_env gl, Pretype_errors.NoOccurrenceFound (if l2r then x else y))) @@ -1134,8 +1134,6 @@ let default_morphism sign m = let mor = resolve_one_typeclass env morph in mor, respect_projection mor morph -let unfold_respectful = lazy (Tactics.unfold_in_concl [[], EvalConstRef (destConst (Lazy.force respectful))]) - VERNAC COMMAND EXTEND AddSetoid1 [ "Add" "Setoid" constr(a) constr(aeq) constr(t) "as" ident(n) ] -> [ init_setoid (); |