From 72dccfa0f5edb59b1ba2668e91828742ab91bb1d Mon Sep 17 00:00:00 2001
From: msozeau
Date: Fri, 18 Jan 2008 00:12:05 +0000
Subject: Change notation for setoid inequality, coerce objects before
 comparing them. Debug tactic redefinition code, streamline Instantiation
 Tactic implementation using that. Have to adapt obligations tactic still.

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10449 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 contrib/interface/xlate.ml | 4 +++-
 1 file changed, 3 insertions(+), 1 deletion(-)

(limited to 'contrib/interface')

diff --git a/contrib/interface/xlate.ml b/contrib/interface/xlate.ml
index 5e82b85bce..6cc7942f8e 100644
--- a/contrib/interface/xlate.ml
+++ b/contrib/interface/xlate.ml
@@ -360,6 +360,8 @@ and (xlate_formula:Topconstr.constr_expr -> Ascent.ct_FORMULA) = function
    | CLambdaN(_,ll,b)-> CT_lambdac(xlate_binder_ne_list ll, xlate_formula b)
    | CLetIn(_, v, a, b) -> 
        CT_letin(CT_def(xlate_id_opt v, xlate_formula a), xlate_formula b)
+   | CLetPattern(_, v, a, b) -> 
+       error "TODO: xlate_formula let | pattern"
    | CAppExpl(_, (Some n, r), l) -> 
        let l', last = decompose_last l in
 	 CT_proj(xlate_formula last,
@@ -2081,7 +2083,7 @@ let rec xlate_vernac =
         xlate_class id2, xlate_class id3)
 
     (* TypeClasses *) 
-   | VernacSetInstantiationTactic _|VernacDeclareInstance _|VernacContext _|
+   | VernacDeclareInstance _|VernacContext _|
 	 VernacInstance (_, _, _)|VernacClass (_, _, _, _, _) ->
 	   xlate_error "TODO: Type Classes commands"
 
-- 
cgit v1.2.3