diff options
| author | ppedrot | 2013-06-27 16:51:52 +0000 |
|---|---|---|
| committer | ppedrot | 2013-06-27 16:51:52 +0000 |
| commit | a1596ac8127071db6c507909bd9723edc720542d (patch) | |
| tree | 854a8532246222a4fcff6818a1cfc7972155c86f /interp | |
| parent | 67a755713eaabf37f4d8e5fd85b4fb04e316938a (diff) | |
Getting rid of IntroPatternArgType.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16610 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'interp')
| -rw-r--r-- | interp/constrarg.ml | 7 |
1 files changed, 6 insertions, 1 deletions
diff --git a/interp/constrarg.ml b/interp/constrarg.ml index 540bca62e6..87da56e4fc 100644 --- a/interp/constrarg.ml +++ b/interp/constrarg.ml @@ -32,7 +32,8 @@ let unsafe_of_type (t : argument_type) : ('a, 'b, 'c) Genarg.genarg_type = let wit_int_or_var = unsafe_of_type IntOrVarArgType -let wit_intro_pattern = unsafe_of_type IntroPatternArgType +let wit_intro_pattern : intro_pattern_expr located uniform_genarg_type = + Genarg.make0 None "intropattern" let wit_ident_gen b = unsafe_of_type (IdentArgType b) @@ -65,3 +66,7 @@ let wit_constr_with_bindings = unsafe_of_type ConstrWithBindingsArgType let wit_bindings = unsafe_of_type BindingsArgType let wit_red_expr = unsafe_of_type RedExprArgType + +(** Register location *) + +let () = register_name0 wit_intro_pattern "Constrarg.wit_intro_pattern" |