aboutsummaryrefslogtreecommitdiffhomepage
path: root/lib
diff options
context:
space:
mode:
authorGravatar Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr>2013-11-25 22:30:02 +0100
committerGravatar Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr>2013-11-30 17:00:34 +0100
commita01a60b366307da3eca63c9937984db6f273dc41 (patch)
treec8a5f42e5db1fd763367390a49d0611a68e33bf5 /lib
parentb86e7c1247fa4b34b75cf20ef24a8e0b6ba6eff1 (diff)
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.
Diffstat (limited to 'lib')
-rw-r--r--lib/genarg.ml6
-rw-r--r--lib/genarg.mli2
2 files changed, 4 insertions, 4 deletions
diff --git a/lib/genarg.ml b/lib/genarg.ml
index 98287d184..0f1e50568 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 e2654fcf5..3d5828bbb 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