From 9c73559b6c7f578e2e7513971f27cf81fc9bfd06 Mon Sep 17 00:00:00 2001
From: herbelin
Date: Thu, 9 Dec 2004 21:06:39 +0000
Subject: Restauration type casted_open_constr pour tactique refine car
 l'unification n'est pas assez puissante pour retarder la coercion vers le but
 au dernier moment

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6458 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 interp/genarg.ml  | 16 ++++++++++++----
 interp/genarg.mli | 10 +++++++++-
 2 files changed, 21 insertions(+), 5 deletions(-)

(limited to 'interp')

diff --git a/interp/genarg.ml b/interp/genarg.ml
index 3483695ecf..2b01a20344 100644
--- a/interp/genarg.ml
+++ b/interp/genarg.ml
@@ -34,7 +34,7 @@ type argument_type =
   | ConstrMayEvalArgType
   | QuantHypArgType
   | TacticArgType
-  | OpenConstrArgType
+  | OpenConstrArgType of bool
   | ConstrWithBindingsArgType
   | BindingsArgType
   | RedExprArgType
@@ -144,9 +144,17 @@ let rawwit_tactic = TacticArgType
 let globwit_tactic = TacticArgType
 let wit_tactic = TacticArgType
 
-let rawwit_open_constr = OpenConstrArgType
-let globwit_open_constr = OpenConstrArgType
-let wit_open_constr = OpenConstrArgType
+let rawwit_open_constr_gen b = OpenConstrArgType b
+let globwit_open_constr_gen b = OpenConstrArgType b 
+let wit_open_constr_gen b = OpenConstrArgType b
+
+let rawwit_open_constr = rawwit_open_constr_gen false
+let globwit_open_constr = globwit_open_constr_gen false
+let wit_open_constr = wit_open_constr_gen false
+
+let rawwit_casted_open_constr = rawwit_open_constr_gen true
+let globwit_casted_open_constr = globwit_open_constr_gen true
+let wit_casted_open_constr = wit_open_constr_gen true
 
 let rawwit_constr_with_bindings = ConstrWithBindingsArgType
 let globwit_constr_with_bindings = ConstrWithBindingsArgType
diff --git a/interp/genarg.mli b/interp/genarg.mli
index 7f01cd6ace..af02a9ebe6 100644
--- a/interp/genarg.mli
+++ b/interp/genarg.mli
@@ -132,10 +132,18 @@ val rawwit_constr_may_eval : ((constr_expr,reference) may_eval,constr_expr,'ta)
 val globwit_constr_may_eval : ((rawconstr_and_expr,evaluable_global_reference and_short_name or_var) may_eval,rawconstr_and_expr,'ta) abstract_argument_type
 val wit_constr_may_eval : (constr,constr,'ta) abstract_argument_type
 
+val rawwit_open_constr_gen : bool -> (open_constr_expr,constr_expr,'ta) abstract_argument_type
+val globwit_open_constr_gen : bool -> (open_rawconstr,rawconstr_and_expr,'ta) abstract_argument_type
+val wit_open_constr_gen : bool -> (open_constr,constr,'ta) abstract_argument_type
+
 val rawwit_open_constr : (open_constr_expr,constr_expr,'ta) abstract_argument_type
 val globwit_open_constr : (open_rawconstr,rawconstr_and_expr,'ta) abstract_argument_type
 val wit_open_constr : (open_constr,constr,'ta) abstract_argument_type
 
+val rawwit_casted_open_constr : (open_constr_expr,constr_expr,'ta) abstract_argument_type
+val globwit_casted_open_constr : (open_rawconstr,rawconstr_and_expr,'ta) abstract_argument_type
+val wit_casted_open_constr : (open_constr,constr,'ta) abstract_argument_type
+
 val rawwit_constr_with_bindings : (constr_expr with_bindings,constr_expr,'ta) abstract_argument_type
 val globwit_constr_with_bindings : (rawconstr_and_expr with_bindings,rawconstr_and_expr,'ta) abstract_argument_type
 val wit_constr_with_bindings : (constr with_bindings,constr,'ta) abstract_argument_type
@@ -227,7 +235,7 @@ type argument_type =
   | ConstrMayEvalArgType
   | QuantHypArgType
   | TacticArgType
-  | OpenConstrArgType
+  | OpenConstrArgType of bool
   | ConstrWithBindingsArgType
   | BindingsArgType
   | RedExprArgType
-- 
cgit v1.2.3