- 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

8 files changed, 25 insertions, 8 deletions

diff --git a/dev/base_include b/dev/base_include
index d4366843f1..711dcb2a1e 100644
--- a/dev/base_include
+++ b/dev/base_include
@@ -14,6 +14,9 @@
 #directory "tactics";;
 #directory "translate";;
 
+#directory "+camlp4";; (* lazy solution: add both of camlp4/5 so that *)
+#directory "+camlp5";; (* Gramext is found in top_printers.ml *)
+
 #use "top_printers.ml";;
 #use "vm_printers.ml";;
 
@@ -112,6 +115,9 @@ open Proof_type
 open Redexpr
 open Refiner
 open Tacmach
+open Decl_proof_instr
+open Tactic_debug
+open Decl_mode
 
 open Auto
 open Autorewrite
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
diff --git a/pretyping/evarutil.ml b/pretyping/evarutil.ml
index 1a7bb2c6cf..e7682285b9 100644
--- a/pretyping/evarutil.ml
+++ b/pretyping/evarutil.ml
@@ -659,7 +659,11 @@ let invert_arg_from_subst env k sigma subst_in_env c_in_env_extended_with_k_bind
 
 let invert_arg env k sigma (evk,args_in_env) c_in_env_extended_with_k_binders =
   let subst_in_env = make_projectable_subst sigma (Evd.find sigma evk) args_in_env in
-  invert_arg_from_subst env k sigma subst_in_env c_in_env_extended_with_k_binders
+  let res = invert_arg_from_subst env k sigma subst_in_env c_in_env_extended_with_k_binders in
+  match res with
+  | Invertible (UniqueProjection (c,_)) when occur_evar evk c -> CannotInvert
+  | _ -> res
+
 
 let effective_projections =
   map_succeed (function Invertible c -> c | _ -> failwith"")
diff --git a/test-suite/output/Notations2.out b/test-suite/output/Notations2.out
index 8a18a9d855..aca872970c 100644
--- a/test-suite/output/Notations2.out
+++ b/test-suite/output/Notations2.out
@@ -1,2 +1,4 @@
 2 3
      : PAIR
+forall (A : Set) (le : A -> A -> Prop) (x y : A), le x y \/ le y x
+     : Prop
diff --git a/test-suite/output/Notations2.v b/test-suite/output/Notations2.v
index 039771d5d5..0d5cc9e24c 100644
--- a/test-suite/output/Notations2.v
+++ b/test-suite/output/Notations2.v
@@ -5,3 +5,7 @@
 Inductive PAIR := P (n1:nat) (n2:nat).
 Coercion P : nat >-> Funclass.
 Check (2 3).
+
+(* Test bug #2091 (variable le was printed using <= !) *)
+
+Check forall (A: Set) (le: A -> A -> Prop) (x y: A), le x y \/ le y x.
diff --git a/test-suite/success/evars.v b/test-suite/success/evars.v
index e3a6e4188b..6764cfa357 100644
--- a/test-suite/success/evars.v
+++ b/test-suite/success/evars.v
@@ -198,7 +198,6 @@ Goal forall x : nat, F1 x -> G1 x.
 refine (fun x H => proj2 (_ x H) _).
 Abort.
 
-
 (* An example from y-not that was failing in 8.2rc1 *)
 
 Fixpoint filter (A:nat->Set) (l:list (sigT A)) : list (sigT A) := 
@@ -207,7 +206,14 @@ Fixpoint filter (A:nat->Set) (l:list (sigT A)) : list (sigT A) :=
   | (existT k v)::l' => (existT _ k v):: (filter A l')
   end.
 
-(* Remark: the following example does not succeed any longer in 8.2 because,
+(* Bug #2000: used to raise Out of memory in 8.2 while it should fail by
+   lack of information on the conclusion of the type of j *)
+
+Goal True.
+set (p:=fun j => j (or_intror _ (fun a:True => j (or_introl _ a)))) || idtac.
+Abort.
+
+(* remark: the following example does not succeed any longer in 8.2 because,
    the algorithm is more general and does exclude a solution that it should
    exclude for typing reason. Handling of types and backtracking is still to
    be done
diff --git a/toplevel/metasyntax.ml b/toplevel/metasyntax.ml
index 75a6a8e755..c0105c8b3b 100644
--- a/toplevel/metasyntax.ml
+++ b/toplevel/metasyntax.ml
@@ -377,7 +377,6 @@ let precedence_of_entry_type from = function
       n, let (lp,rp) = prec_assoc a in if b=Left then lp else rp
   | ETConstr (NumLevel n,InternalProd) -> n, Prec n
   | ETConstr (NextLevel,_) -> from, L
-  | ETOther ("constr","annot") -> 10, Prec 10
   | _ -> 0, E (* ?? *)
 
 (* Some breaking examples *)