- Fixing #2090 (occur check missing when trying to solve evar-evar equation).

- Adding test file related to commit 12080 (bug #2091).
- Cleaning old parsing stuff from 8.0.
- Support for camlp5 in base_include.



git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12106 85f007b7-540e-0410-9357-904b9bb8a0f7

2 files changed, 0 insertions, 4 deletions

diff --git a/parsing/pcoq.ml4 b/parsing/pcoq.ml4
index 1e5b21ec48..8f75675957 100644
--- a/parsing/pcoq.ml4
+++ b/parsing/pcoq.ml4
@@ -437,7 +437,6 @@ module Constr =
     let global = make_gen_entry uconstr rawwit_ref "global"
     let sort = make_gen_entry uconstr rawwit_sort "sort"
     let pattern = Gram.Entry.create "constr:pattern"
-    let annot = Gram.Entry.create "constr:annot"
     let constr_pattern = gec_constr "constr_pattern"
     let lconstr_pattern = gec_constr "lconstr_pattern"
     let binder = Gram.Entry.create "constr:binder"
@@ -694,8 +693,6 @@ let compute_entry allow_create adjust forpat = function
   | ETBigint -> weaken_entry Prim.bigint, None, false
   | ETReference -> weaken_entry Constr.global, None, false
   | ETPattern -> weaken_entry Constr.pattern, None, false
-  | ETOther ("constr","annot") -> 
-      weaken_entry Constr.annot, None, false
   | ETConstrList _ -> error "List of entries cannot be registered."
   | ETOther (u,n) ->
       let u = get_univ u in
diff --git a/parsing/pcoq.mli b/parsing/pcoq.mli
index f084c74f0b..97a47dcc45 100644
--- a/parsing/pcoq.mli
+++ b/parsing/pcoq.mli
@@ -159,7 +159,6 @@ module Constr :
     val global : reference Gram.Entry.e
     val sort : rawsort Gram.Entry.e
     val pattern : cases_pattern_expr Gram.Entry.e
-    val annot : constr_expr Gram.Entry.e
     val constr_pattern : constr_expr Gram.Entry.e
     val lconstr_pattern : constr_expr Gram.Entry.e
     val binder : (name located list * binder_kind * constr_expr) Gram.Entry.e