diff options
| author |  ppedrot <ppedrot@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2013-07-05 19:22:49 +0000 |
|---|---|---|
| committer | ppedrot <ppedrot@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2013-07-05 19:22:49 +0000 |
| commit | 931bd73212b0095d8c50e0355ee66faa32bf8db6 (patch) | |
| tree | fbff2b6bf249899f4cdcd6d2a821d5259c177d7b /tactics/tacintern.ml | |
| parent | a778b72e3ebfbe784fbe55ee5e124ba3f66cfb10 (diff) | |
Removing SortArgType.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16618 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'tactics/tacintern.ml')
| -rw-r--r-- | tactics/tacintern.ml | 8 |
1 files changed, 4 insertions, 4 deletions
diff --git a/tactics/tacintern.ml b/tactics/tacintern.ml index d176c516f..dbe8b8dd7 100644 --- a/tactics/tacintern.ml +++ b/tactics/tacintern.ml @@ -768,8 +768,6 @@ and intern_genarg ist x = in_gen (glbwit wit_ref) (intern_global_reference ist (out_gen (rawwit wit_ref) x)) | GenArgType -> in_gen (glbwit wit_genarg) (intern_genarg ist (out_gen (rawwit wit_genarg) x)) - | SortArgType -> - in_gen (glbwit wit_sort) (out_gen (rawwit wit_sort) x) | ConstrArgType -> in_gen (glbwit wit_constr) (intern_constr ist (out_gen (rawwit wit_constr) x)) | ConstrMayEvalArgType -> @@ -937,6 +935,8 @@ let add_tacdef local isrec tacl = (** Registering *) +let lift intern = (); fun ist x -> (ist, intern ist x) + let () = let intern_intro_pattern ist pat = let lf = ref Id.Set.empty in @@ -947,8 +947,8 @@ let () = Genintern.register_intern0 wit_intro_pattern intern_intro_pattern let () = - let intern ist tac = (ist, intern_tactic_or_tacarg ist tac) in - Genintern.register_intern0 wit_tactic intern + Genintern.register_intern0 wit_tactic (lift intern_tactic_or_tacarg); + Genintern.register_intern0 wit_sort (fun ist s -> (ist, s)) (***************************************************************************) (* Backwarding recursive needs of tactic glob/interp/eval functions *) |