diff options
author | Emilio Jesus Gallego Arias <e+git@x80.org> | 2018-05-22 00:07:26 +0200 |
---|---|---|
committer | Emilio Jesus Gallego Arias <e+git@x80.org> | 2018-06-12 14:42:28 +0200 |
commit | 368a25e4ef14512b00f5799e26c3f615bc540201 (patch) | |
tree | 29602372307ff70f2a7b06f0a27609a73caa5666 /vernac/g_vernac.ml4 | |
parent | 36a98d55576ebdb106a55c3bd682961da8d77dee (diff) |
[api] Misctypes removal: several moves:
- move_location to proofs/logic.
- intro_pattern_naming to Namegen.
Diffstat (limited to 'vernac/g_vernac.ml4')
-rw-r--r-- | vernac/g_vernac.ml4 | 8 |
1 files changed, 5 insertions, 3 deletions
diff --git a/vernac/g_vernac.ml4 b/vernac/g_vernac.ml4 index b6523981c..59449d07a 100644 --- a/vernac/g_vernac.ml4 +++ b/vernac/g_vernac.ml4 @@ -12,6 +12,7 @@ open Pp open CErrors open Util open Names +open Glob_term open Vernacexpr open Constrexpr open Constrexpr_ops @@ -20,6 +21,7 @@ open Decl_kinds open Declaremods open Declarations open Misctypes +open Namegen open Tok (* necessary for camlp5 *) open Pcoq @@ -338,7 +340,7 @@ GEXTEND Gram ; type_cstr: [ [ ":"; c=lconstr -> c - | -> CAst.make ~loc:!@loc @@ CHole (None, Misctypes.IntroAnonymous, None) ] ] + | -> CAst.make ~loc:!@loc @@ CHole (None, IntroAnonymous, None) ] ] ; (* Inductive schemes *) scheme: @@ -394,7 +396,7 @@ GEXTEND Gram (None,DefExpr(id,mkCLambdaN ~loc:!@loc l b,None)) ] ] ; record_binder: - [ [ id = name -> (None,AssumExpr(id, CAst.make ~loc:!@loc @@ CHole (None, Misctypes.IntroAnonymous, None))) + [ [ id = name -> (None,AssumExpr(id, CAst.make ~loc:!@loc @@ CHole (None, IntroAnonymous, None))) | id = name; f = record_binder_body -> f id ] ] ; assum_list: @@ -413,7 +415,7 @@ GEXTEND Gram t= [ coe = of_type_with_opt_coercion; c = lconstr -> fun l id -> (not (Option.is_empty coe),(id,mkCProdN ~loc:!@loc l c)) | -> - fun l id -> (false,(id,mkCProdN ~loc:!@loc l (CAst.make ~loc:!@loc @@ CHole (None, Misctypes.IntroAnonymous, None)))) ] + fun l id -> (false,(id,mkCProdN ~loc:!@loc l (CAst.make ~loc:!@loc @@ CHole (None, IntroAnonymous, None)))) ] -> t l ]] ; |