From f39cd683cb022d877a0d2ebd014fa0879bc6de00 Mon Sep 17 00:00:00 2001
From: herbelin
Date: Mon, 6 Dec 2004 11:28:22 +0000
Subject: Généralisation de CastedOpenConstrArg en OpenConstrArg, à charge des
 tactiques d'appliquer une éventuelle coercion vers le but

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6408 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 interp/genarg.ml | 12 ++++++------
 1 file changed, 6 insertions(+), 6 deletions(-)

(limited to 'interp/genarg.ml')

diff --git a/interp/genarg.ml b/interp/genarg.ml
index 91b8c5bf74..3483695ecf 100644
--- a/interp/genarg.ml
+++ b/interp/genarg.ml
@@ -34,7 +34,7 @@ type argument_type =
   | ConstrMayEvalArgType
   | QuantHypArgType
   | TacticArgType
-  | CastedOpenConstrArgType
+  | OpenConstrArgType
   | ConstrWithBindingsArgType
   | BindingsArgType
   | RedExprArgType
@@ -85,8 +85,8 @@ and pr_case_intro_pattern = function
       ++ str "]"
 
 type open_constr = Evd.evar_map * Term.constr
-type open_constr_expr = constr_expr
-type open_rawconstr = rawconstr_and_expr
+type open_constr_expr = unit * constr_expr
+type open_rawconstr = unit * rawconstr_and_expr
 
 let rawwit_bool = BoolArgType
 let globwit_bool = BoolArgType
@@ -144,9 +144,9 @@ let rawwit_tactic = TacticArgType
 let globwit_tactic = TacticArgType
 let wit_tactic = TacticArgType
 
-let rawwit_casted_open_constr = CastedOpenConstrArgType
-let globwit_casted_open_constr = CastedOpenConstrArgType
-let wit_casted_open_constr = CastedOpenConstrArgType
+let rawwit_open_constr = OpenConstrArgType
+let globwit_open_constr = OpenConstrArgType
+let wit_open_constr = OpenConstrArgType
 
 let rawwit_constr_with_bindings = ConstrWithBindingsArgType
 let globwit_constr_with_bindings = ConstrWithBindingsArgType
-- 
cgit v1.2.3