From ff7e6f61796c9afbeb89cc9ab5c6eb459408dbf4 Mon Sep 17 00:00:00 2001
From: msozeau
Date: Thu, 23 Oct 2008 22:09:08 +0000
Subject: Fix bug #1977 by allowing the [apply] variants to take an
 [open_constr] instead of a completely resolved [constr] as input. The
 propagation of the evars associated to the lemma is only allowed when the
 evar flag is on (i.e. for [eapply]), otherwise they should be resolved by the
 end of the application. Should be completely backwards compatible...

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

(limited to 'contrib/interface')

diff --git a/contrib/interface/xlate.ml b/contrib/interface/xlate.ml
index 4e910935a9..7b654b74b7 100644
--- a/contrib/interface/xlate.ml
+++ b/contrib/interface/xlate.ml
@@ -375,6 +375,7 @@ and (xlate_formula:Topconstr.constr_expr -> Ascent.ct_FORMULA) = function
 		 (xlate_formula f, List.map xlate_formula_expl l'))
    | CApp(_, (_,f), l) -> 
        CT_appc(xlate_formula f, xlate_formula_expl_ne_list l)
+   | CRecord (_,_,_) -> xlate_error "CRecord: TODO"
    | CCases (_, _, _, [], _) -> assert false
    | CCases (_, _, ret_type, tm::tml, eqns)->
        CT_cases(CT_matched_formula_ne_list(xlate_matched_formula tm,
-- 
cgit v1.2.3