diff options
Diffstat (limited to 'interp')
-rw-r--r-- | interp/constrarg.ml | 3 | ||||
-rw-r--r-- | interp/constrarg.mli | 2 | ||||
-rw-r--r-- | interp/constrintern.ml | 11 | ||||
-rw-r--r-- | interp/constrintern.mli | 2 |
4 files changed, 13 insertions, 5 deletions
diff --git a/interp/constrarg.ml b/interp/constrarg.ml index c25e02c02..cb980f5a3 100644 --- a/interp/constrarg.ml +++ b/interp/constrarg.ml @@ -47,6 +47,8 @@ let wit_constr = unsafe_of_type ConstrArgType let wit_constr_may_eval = unsafe_of_type ConstrMayEvalArgType +let wit_uconstr = Genarg.make0 None "uconstr" + let wit_open_constr = unsafe_of_type OpenConstrArgType let wit_constr_with_bindings = unsafe_of_type ConstrWithBindingsArgType @@ -65,4 +67,5 @@ let () = register_name0 wit_intro_pattern "Constrarg.wit_intro_pattern"; register_name0 wit_tactic "Constrarg.wit_tactic"; register_name0 wit_sort "Constrarg.wit_sort"; + register_name0 wit_uconstr "Constrarg.uconstr"; register_name0 wit_clause_dft_concl "Constrarg.wit_clause_dft_concl"; diff --git a/interp/constrarg.mli b/interp/constrarg.mli index 983163ec1..a97ccb270 100644 --- a/interp/constrarg.mli +++ b/interp/constrarg.mli @@ -50,6 +50,8 @@ val wit_constr_may_eval : (glob_constr_and_expr,evaluable_global_reference and_short_name or_var,glob_constr_pattern_and_expr) may_eval, constr) genarg_type +val wit_uconstr : (constr_expr , glob_constr_and_expr, Glob_term.glob_constr) genarg_type + val wit_open_constr : (open_constr_expr, open_glob_constr, Evd.open_constr) genarg_type diff --git a/interp/constrintern.ml b/interp/constrintern.ml index 7ca4d70c3..5d77c4669 100644 --- a/interp/constrintern.ml +++ b/interp/constrintern.ml @@ -638,7 +638,7 @@ let string_of_ty = function | Variable -> "var" let intern_var genv (ltacvars,ntnvars) namedctx loc id = - let (ltacvars,unbndltacvars) = ltacvars in + let (ltacvars,unbndltacvars,ltacsubst) = ltacvars in (* Is [id] an inductive type potentially with implicit *) try let ty,expl_impls,impls,argsc = Id.Map.find id genv.impls in @@ -652,6 +652,9 @@ let intern_var genv (ltacvars,ntnvars) namedctx loc id = if Id.Set.mem id genv.ids || Id.Set.mem id ltacvars then GVar (loc,id), [], [], [] + (* Is [id] bound to a glob_constr in the the ltac context *) + else if Id.Map.mem id ltacsubst then + Id.Map.find id ltacsubst, [], [], [] (* Is [id] a notation variable *) else if Id.Map.mem id ntnvars then @@ -1549,7 +1552,7 @@ let internalize globalenv env allow_patvar lvar c = let solve = match solve with | None -> None | Some gen -> - let ((cvars, lvars), ntnvars) = lvar in + let ((cvars, lvars,_), ntnvars) = lvar in let ntnvars = Id.Map.domain ntnvars in let lvars = Id.Set.union lvars cvars in let lvars = Id.Set.union lvars ntnvars in @@ -1769,9 +1772,9 @@ let scope_of_type_kind = function | OfType typ -> compute_type_scope typ | WithoutTypeConstraint -> None -type ltac_sign = Id.Set.t * Id.Set.t +type ltac_sign = Id.Set.t * Id.Set.t * glob_constr Id.Map.t -let empty_ltac_sign = (Id.Set.empty, Id.Set.empty) +let empty_ltac_sign = (Id.Set.empty, Id.Set.empty, Id.Map.empty) let intern_gen kind env ?(impls=empty_internalization_env) ?(allow_patvar=false) ?(ltacvars=empty_ltac_sign) diff --git a/interp/constrintern.mli b/interp/constrintern.mli index 1331fd968..2b61c51dc 100644 --- a/interp/constrintern.mli +++ b/interp/constrintern.mli @@ -67,7 +67,7 @@ val compute_internalization_env : env -> var_internalization_type -> Id.t list -> types list -> Impargs.manual_explicitation list list -> internalization_env -type ltac_sign = Id.Set.t * Id.Set.t +type ltac_sign = Id.Set.t * Id.Set.t * glob_constr Id.Map.t type glob_binder = (Name.t * binding_kind * glob_constr option * glob_constr) |