diff options
Diffstat (limited to 'interp/genarg.ml')
| -rw-r--r-- | interp/genarg.ml | 26 |
1 files changed, 15 insertions, 11 deletions
diff --git a/interp/genarg.ml b/interp/genarg.ml index a9adbe83..41cbcdaf 100644 --- a/interp/genarg.ml +++ b/interp/genarg.ml @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2012 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2014 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) @@ -32,7 +32,7 @@ type argument_type = | ConstrArgType | ConstrMayEvalArgType | QuantHypArgType - | OpenConstrArgType of bool + | OpenConstrArgType of bool * bool (* casted, TC resolution *) | ConstrWithBindingsArgType | BindingsArgType | RedExprArgType @@ -156,17 +156,21 @@ let rawwit_constr_may_eval = ConstrMayEvalArgType let globwit_constr_may_eval = ConstrMayEvalArgType let wit_constr_may_eval = ConstrMayEvalArgType -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_gen (b1,b2) = OpenConstrArgType (b1,b2) +let globwit_open_constr_gen (b1,b2) = OpenConstrArgType (b1,b2) +let wit_open_constr_gen (b1,b2) = OpenConstrArgType (b1,b2) -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_open_constr = rawwit_open_constr_gen (false,false) +let globwit_open_constr = globwit_open_constr_gen (false,false) +let wit_open_constr = wit_open_constr_gen (false,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_casted_open_constr = rawwit_open_constr_gen (true,false) +let globwit_casted_open_constr = globwit_open_constr_gen (true,false) +let wit_casted_open_constr = wit_open_constr_gen (true,false) + +let rawwit_open_constr_wTC = rawwit_open_constr_gen (false,true) +let globwit_open_constr_wTC = globwit_open_constr_gen (false,true) +let wit_open_constr_wTC = wit_open_constr_gen (false,true) let rawwit_constr_with_bindings = ConstrWithBindingsArgType let globwit_constr_with_bindings = ConstrWithBindingsArgType |