From 0df8820d7fbdd21c46b2b2945b25d770a40de463 Mon Sep 17 00:00:00 2001
From: herbelin
Date: Sun, 21 Sep 2003 22:44:27 +0000
Subject: Mise en place d'implicites par noms en v8

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

(limited to 'contrib/interface')

diff --git a/contrib/interface/xlate.ml b/contrib/interface/xlate.ml
index 88e419fa6f..ec9e88c773 100644
--- a/contrib/interface/xlate.ml
+++ b/contrib/interface/xlate.ml
@@ -378,7 +378,10 @@ and (xlate_formula:Topconstr.constr_expr -> Ascent.ct_FORMULA) = function
    | CFix _ -> assert false
 and xlate_formula_expl = function
     (a, None) -> xlate_formula a
-  | (a, i) -> CT_bang(xlate_int_opt i, xlate_formula a)
+  | (a, Some (_,ExplByPos i)) -> 
+      CT_bang(xlate_int_opt (Some i), xlate_formula a)
+  | (a, Some (_,ExplByName i)) ->
+      xlate_error "TODO: explicitation of implicit by name"
 and xlate_formula_expl_ne_list = function
     [] -> assert false
   | a::l -> CT_formula_ne_list(xlate_formula_expl a, List.map xlate_formula_expl l)
-- 
cgit v1.2.3