diff options
| author | msozeau | 2008-01-18 00:12:05 +0000 |
|---|---|---|
| committer | msozeau | 2008-01-18 00:12:05 +0000 |
| commit | 72dccfa0f5edb59b1ba2668e91828742ab91bb1d (patch) | |
| tree | 46339464eee6a725dc9ae10d38bd8ae45e724e44 /contrib/interface | |
| parent | edbb81e324234548c2bb70306fb448420e1bbd70 (diff) | |
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
Diffstat (limited to 'contrib/interface')
| -rw-r--r-- | contrib/interface/xlate.ml | 4 |
1 files changed, 3 insertions, 1 deletions
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" |