diff options
| -rw-r--r-- | dev/base_include | 6 | ||||
| -rw-r--r-- | parsing/pcoq.ml4 | 3 | ||||
| -rw-r--r-- | parsing/pcoq.mli | 1 | ||||
| -rw-r--r-- | pretyping/evarutil.ml | 6 | ||||
| -rw-r--r-- | test-suite/output/Notations2.out | 2 | ||||
| -rw-r--r-- | test-suite/output/Notations2.v | 4 | ||||
| -rw-r--r-- | test-suite/success/evars.v | 10 | ||||
| -rw-r--r-- | toplevel/metasyntax.ml | 1 |
8 files changed, 25 insertions, 8 deletions
diff --git a/dev/base_include b/dev/base_include index d4366843f..711dcb2a1 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 1e5b21ec4..8f7567595 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 f084c74f0..97a47dcc4 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 1a7bb2c6c..e7682285b 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 8a18a9d85..aca872970 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 039771d5d..0d5cc9e24 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 e3a6e4188..6764cfa35 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 75a6a8e75..c0105c8b3 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 *) |