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
---
 parsing/argextend.ml4 | 6 +++---
 1 file changed, 3 insertions(+), 3 deletions(-)

(limited to 'parsing/argextend.ml4')

diff --git a/parsing/argextend.ml4 b/parsing/argextend.ml4
index df48f5d8de..78128a99d8 100644
--- a/parsing/argextend.ml4
+++ b/parsing/argextend.ml4
@@ -33,7 +33,7 @@ let rec make_rawwit loc = function
   | QuantHypArgType -> <:expr< Genarg.rawwit_quant_hyp >>
   | TacticArgType -> <:expr< Genarg.rawwit_tactic >>
   | RedExprArgType -> <:expr< Genarg.rawwit_red_expr >>
-  | CastedOpenConstrArgType -> <:expr< Genarg.rawwit_casted_open_constr >>
+  | OpenConstrArgType -> <:expr< Genarg.rawwit_open_constr >>
   | ConstrWithBindingsArgType -> <:expr< Genarg.rawwit_constr_with_bindings >>
   | BindingsArgType -> <:expr< Genarg.rawwit_bindings >>
   | List0ArgType t -> <:expr< Genarg.wit_list0 $make_rawwit loc t$ >>
@@ -59,7 +59,7 @@ let rec make_globwit loc = function
   | ConstrMayEvalArgType -> <:expr< Genarg.globwit_constr_may_eval >>
   | TacticArgType -> <:expr< Genarg.globwit_tactic >>
   | RedExprArgType -> <:expr< Genarg.globwit_red_expr >>
-  | CastedOpenConstrArgType -> <:expr< Genarg.globwit_casted_open_constr >>
+  | OpenConstrArgType -> <:expr< Genarg.globwit_open_constr >>
   | ConstrWithBindingsArgType -> <:expr< Genarg.globwit_constr_with_bindings >>
   | BindingsArgType -> <:expr< Genarg.globwit_bindings >>
   | List0ArgType t -> <:expr< Genarg.wit_list0 $make_globwit loc t$ >>
@@ -85,7 +85,7 @@ let rec make_wit loc = function
   | ConstrMayEvalArgType -> <:expr< Genarg.wit_constr_may_eval >>
   | TacticArgType -> <:expr< Genarg.wit_tactic >>
   | RedExprArgType -> <:expr< Genarg.wit_red_expr >>
-  | CastedOpenConstrArgType -> <:expr< Genarg.wit_casted_open_constr >>
+  | OpenConstrArgType -> <:expr< Genarg.wit_open_constr >>
   | ConstrWithBindingsArgType -> <:expr< Genarg.wit_constr_with_bindings >>
   | BindingsArgType -> <:expr< Genarg.wit_bindings >>
   | List0ArgType t -> <:expr< Genarg.wit_list0 $make_wit loc t$ >>
-- 
cgit v1.2.3