From a01a60b366307da3eca63c9937984db6f273dc41 Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Mon, 25 Nov 2013 22:30:02 +0100
Subject: Getting rid of casted_open_constr. It was only used by the refine
 tactic, which now uses plain glob_constr's. Now there is no real need to
 depend on goal when interpreting genargs.

Possible minor incompatibilities:

1. The interpretation of glob_constr to constr is now done by
Goal.constr_of_raw, which may be slightly dumbier than the dedicated
Tacinterp.interp_open_constr which tries harder. Stdlib and test-suite
do go through, though.

2. I had to change the parsing level of wit_glob in Extraargs
from lconstr to constr. It may break ML notations using glob, but
as they are only used inside Coq code and all well-parenthezised,
it should be OK.
---
 lib/genarg.ml  | 6 +++---
 lib/genarg.mli | 2 +-
 2 files changed, 4 insertions(+), 4 deletions(-)

(limited to 'lib')

diff --git a/lib/genarg.ml b/lib/genarg.ml
index 98287d1842..0f1e50568d 100644
--- a/lib/genarg.ml
+++ b/lib/genarg.ml
@@ -20,7 +20,7 @@ type argument_type =
   | ConstrArgType
   | ConstrMayEvalArgType
   | QuantHypArgType
-  | OpenConstrArgType of bool
+  | OpenConstrArgType
   | ConstrWithBindingsArgType
   | BindingsArgType
   | RedExprArgType
@@ -38,7 +38,7 @@ let rec argument_type_eq arg1 arg2 = match arg1, arg2 with
 | ConstrArgType, ConstrArgType -> true
 | ConstrMayEvalArgType, ConstrMayEvalArgType -> true
 | QuantHypArgType, QuantHypArgType -> true
-| OpenConstrArgType b1, OpenConstrArgType b2 -> (b1 : bool) == b2
+| OpenConstrArgType, OpenConstrArgType -> true
 | ConstrWithBindingsArgType, ConstrWithBindingsArgType -> true
 | BindingsArgType, BindingsArgType -> true
 | RedExprArgType, RedExprArgType -> true
@@ -59,7 +59,7 @@ let rec pr_argument_type = function
 | ConstrArgType -> str "constr"
 | ConstrMayEvalArgType -> str "constr_may_eval"
 | QuantHypArgType -> str "qhyp"
-| OpenConstrArgType _ -> str "open_constr"
+| OpenConstrArgType -> str "open_constr"
 | ConstrWithBindingsArgType -> str "constr_with_bindings"
 | BindingsArgType -> str "bindings"
 | RedExprArgType -> str "redexp"
diff --git a/lib/genarg.mli b/lib/genarg.mli
index e2654fcf57..3d5828bbbc 100644
--- a/lib/genarg.mli
+++ b/lib/genarg.mli
@@ -199,7 +199,7 @@ type argument_type =
   | ConstrArgType
   | ConstrMayEvalArgType
   | QuantHypArgType
-  | OpenConstrArgType of bool
+  | OpenConstrArgType
   | ConstrWithBindingsArgType
   | BindingsArgType
   | RedExprArgType
-- 
cgit v1.2.3


From cb290d81c46ec370e303e1414e203c40c8fa1174 Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Sun, 1 Dec 2013 18:47:55 +0100
Subject: Removing RefArgType generic argument.

---
 lib/genarg.ml  | 3 ---
 lib/genarg.mli | 1 -
 2 files changed, 4 deletions(-)

(limited to 'lib')

diff --git a/lib/genarg.ml b/lib/genarg.ml
index 0f1e50568d..6520669fa6 100644
--- a/lib/genarg.ml
+++ b/lib/genarg.ml
@@ -14,7 +14,6 @@ type argument_type =
   | IntOrVarArgType
   | IdentArgType of bool
   | VarArgType
-  | RefArgType
   (* Specific types *)
   | GenArgType
   | ConstrArgType
@@ -33,7 +32,6 @@ let rec argument_type_eq arg1 arg2 = match arg1, arg2 with
 | IntOrVarArgType, IntOrVarArgType -> true
 | IdentArgType b1, IdentArgType b2 -> (b1 : bool) == b2
 | VarArgType, VarArgType -> true
-| RefArgType, RefArgType -> true
 | GenArgType, GenArgType -> true
 | ConstrArgType, ConstrArgType -> true
 | ConstrMayEvalArgType, ConstrMayEvalArgType -> true
@@ -54,7 +52,6 @@ let rec pr_argument_type = function
 | IdentArgType true -> str "ident"
 | IdentArgType false -> str "pattern_ident"
 | VarArgType -> str "var"
-| RefArgType -> str "ref"
 | GenArgType -> str "genarg"
 | ConstrArgType -> str "constr"
 | ConstrMayEvalArgType -> str "constr_may_eval"
diff --git a/lib/genarg.mli b/lib/genarg.mli
index 3d5828bbbc..51c261742e 100644
--- a/lib/genarg.mli
+++ b/lib/genarg.mli
@@ -193,7 +193,6 @@ type argument_type =
   | IntOrVarArgType
   | IdentArgType of bool
   | VarArgType
-  | RefArgType
   (** Specific types *)
   | GenArgType
   | ConstrArgType
-- 
cgit v1.2.3