summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
authorGravatar Stephane Glondu <steph@glondu.net>2012-03-27 07:41:19 +0200
committerGravatar Stephane Glondu <steph@glondu.net>2012-03-27 07:41:19 +0200
commit2bdcd093b357adb2185518dabbafd1a0b9279044 (patch)
treebb98a3f549ff7fb9721a94972f0baba47290fedb
parent300293c119981054c95182a90c829058530a6b6f (diff)
Imported Upstream version 8.3.pl4upstream/8.3.pl4
-rw-r--r--.gitignore107
-rw-r--r--CHANGES33
-rw-r--r--checker/checker.ml2
-rwxr-xr-xconfigure4
-rw-r--r--ide/coq.ml8
-rw-r--r--ide/coqide.ml8
-rw-r--r--interp/constrintern.ml10
-rw-r--r--interp/notation.ml2
-rw-r--r--interp/topconstr.ml8
-rw-r--r--interp/topconstr.mli6
-rw-r--r--kernel/term.mli5
-rw-r--r--kernel/univ.ml113
-rw-r--r--kernel/univ.mli6
-rw-r--r--lib/compat.ml44
-rw-r--r--library/impargs.ml15
-rw-r--r--man/coqtop.12
-rw-r--r--parsing/egrammar.ml38
-rw-r--r--parsing/ppvernac.ml4
-rw-r--r--parsing/tacextend.ml444
-rw-r--r--plugins/funind/recdef.ml5
-rw-r--r--plugins/romega/ReflOmegaCore.v2
-rw-r--r--plugins/subtac/subtac_obligations.ml4
-rw-r--r--pretyping/cases.ml4
-rw-r--r--pretyping/clenv.ml9
-rw-r--r--pretyping/detyping.ml10
-rw-r--r--pretyping/inductiveops.ml21
-rw-r--r--pretyping/namegen.ml47
-rw-r--r--pretyping/namegen.mli7
-rw-r--r--pretyping/pretype_errors.ml4
-rw-r--r--pretyping/typeclasses_errors.ml6
-rw-r--r--pretyping/vnorm.ml11
-rw-r--r--proofs/logic.ml4
-rw-r--r--proofs/refiner.ml14
-rw-r--r--tactics/class_tactics.ml44
-rw-r--r--tactics/extratactics.ml44
-rw-r--r--tactics/rewrite.ml42
-rw-r--r--tactics/tacinterp.ml22
-rw-r--r--tools/coqdoc/cpretty.mll14
-rw-r--r--toplevel/cerrors.ml8
-rw-r--r--toplevel/toplevel.ml8
-rw-r--r--toplevel/vernac.ml12
41 files changed, 314 insertions, 327 deletions
diff --git a/.gitignore b/.gitignore
deleted file mode 100644
index 031b06b5..00000000
--- a/.gitignore
+++ /dev/null
@@ -1,107 +0,0 @@
-*.glob
-*.d
-*.d.raw
-*.vo
-*.cm*
-*.annot
-*.spit
-*.spot
-*.o
-*.a
-*.log
-*.aux
-*.dvi
-*.blg
-*.bbl
-*.idx
-*.ilg
-*.toc
-*.atoc
-*.comidx
-*.comind
-*.erridx
-*.errind
-*.haux
-*.hcomind
-*.herrind
-*.hind
-*.htacind
-*.htoc
-*.ind
-*.lof
-*.stamp
-*.tacidx
-*.tacind
-*.v.tex
-*.v.pdf
-*.v.ps
-*.v.html
-revision
-TAGS
-bin/
-config/Makefile
-config/coq_config.ml
-plugins/dp/dp_zenon.ml
-dev/ocamldebug-coq
-dev/ocamlweb-doc/lex.ml
-dev/ocamlweb-doc/syntax.ml
-dev/ocamlweb-doc/syntax.mli
-ide/config_lexer.ml
-ide/config_parser.ml
-ide/config_parser.mli
-ide/coq_lex.ml
-ide/extract_index.ml
-ide/find_phrase.ml
-ide/highlight.ml
-ide/undo.mli
-ide/utf8_convert.ml
-kernel/byterun/coq_jumptbl.h
-kernel/byterun/dllcoqrun.so
-kernel/copcodes.ml
-scripts/tolink.ml
-states/initial.coq
-test-suite/lia.cache
-test-suite/trace
-theories/Numbers/Natural/BigN/NMake_gen.v
-tools/coqdep_lexer.ml
-tools/coqdoc/cpretty.ml
-tools/coqwc.ml
-tools/gallina_lexer.ml
-toplevel/mltop.optml
-plugins/micromega/csdpcert
-toplevel/mltop.byteml
-coqdoc.sty
-ide/index_urls.txt
-doc/faq/html/
-doc/refman/csdp.cache
-doc/refman/trace
-doc/refman/Reference-Manual.pdf
-doc/refman/Reference-Manual.ps
-doc/refman/cover.html
-doc/refman/styles.hva
-doc/refman/Reference-Manual.html
-doc/common/version.tex
-doc/refman/Reference-Manual.sh
-doc/refman/coqide-queries.eps
-doc/refman/coqide.eps
-doc/refman/euclid.ml
-doc/refman/euclid.mli
-doc/refman/heapsort.ml
-doc/refman/heapsort.mli
-doc/refman/html/
-doc/stdlib/Library.out
-doc/stdlib/Library.pdf
-doc/stdlib/Library.ps
-doc/stdlib/Library.coqdoc.tex
-doc/stdlib/html/
-doc/stdlib/index-body.html
-doc/stdlib/index-list.html
-doc/RecTutorial/RecTutorial.html
-doc/RecTutorial/RecTutorial.pdf
-doc/RecTutorial/RecTutorial.ps
-dev/doc/naming-conventions.pdf
-_build
-plugins/*/*_mod.ml
-myocamlbuild_config.ml
-.DS_Store
-.pc
diff --git a/CHANGES b/CHANGES
index b8a5f9ea..954231f8 100644
--- a/CHANGES
+++ b/CHANGES
@@ -1,10 +1,36 @@
+Changes from V8.3pl3 to V8.3pl4
+===============================
+
+Bug fixes:
+
+- #2724 (using notations with binders in cases patterns was provoking an anomaly)
+- #2723 (alpha-conversion bug #2723 introduced in r12485-12486)
+- #2732 (anomaly when using the tolerance for writing "f atomic_tac"
+ as a short-hand for "f ltac:(atomic_tac)")
+- #2729 (vm_compute: function used to decompose constructors did not handle let-ins)
+- #2728 (compatibility with camlp5 6.05)
+- #2682 (Fail discard the effects of a successful command)
+- #2703 (Undetected universe inconsistency)
+- #2667 (Coq crashes when "Arguments Scope" has too many parameters)
+- Compilation of coqide under MacOS with gtk >= 2.24.11
+- Coqdoc: Fixing missing newline when using "Proof term."
+
+
Changes from V8.3pl2 to V8.3pl3
===============================
+The following (non exhaustive) list of bugs have been fixed:
+
General
- #2411 (Axiom / Hypothesis / Variable allowed again during proofs)
- #2603 (verify that all names of an inductive block aren't already used)
+- #1804 (pattern-matching compilation bug with highly nested sigma-types)
+- #2615 (anomaly in inferring pattern-matching return type)
+- #2504 (bug in computing universe of polymorphic inductive types)
+- #2407 (stack overflow in Function)
+- #2181 (unnamed but dependent fields in Classes)
+- bug with modules in virtual machine
Modules
@@ -17,6 +43,7 @@ Tactics
- #2467, #2464 (fixes for fsetdec)
- Document the "appcontext" variant of "context" that better handles
partial applications.
+- #2640 (ltac anomaly in expecting a tactic and finding a definition)
Coqide
@@ -35,6 +62,12 @@ Extraction
- Forbid Prop-universe-polymorphism of inductive when extracting
to ocaml, otherwise things may fail badly (report by S. Glondu).
+Coqdoc
+
+- #2606 (bad processing of coq escaped in comments)
+- #2423 (handling of -R in coqdoc)
+- fixing garbage when using some greek letters as identifier names
+
Changes from V8.3pl1 to V8.3pl2
===============================
diff --git a/checker/checker.ml b/checker/checker.ml
index 76f81264..c8cb58ae 100644
--- a/checker/checker.ml
+++ b/checker/checker.ml
@@ -274,7 +274,7 @@ let rec explain_exn = function
(* let ctx = Check.get_env() in
hov 0
(str "Error:" ++ spc () ++ Himsg.explain_inductive_error ctx e)*)
- | Stdpp.Exc_located (loc,exc) ->
+ | Compat.Exc_located (loc,exc) ->
hov 0 ((if loc = dummy_loc then (mt ())
else (str"At location " ++ print_loc loc ++ str":" ++ fnl ()))
++ explain_exn exc)
diff --git a/configure b/configure
index 8498bd70..16b2a82a 100755
--- a/configure
+++ b/configure
@@ -6,7 +6,7 @@
#
##################################
-VERSION=8.3pl3
+VERSION=8.3pl4
VOMAGIC=08300
STATEMAGIC=58300
DATE=`LANG=C date +"%B %Y"`
@@ -1085,4 +1085,4 @@ echo
echo "*Warning* To compile the system for a new architecture"
echo " don't forget to do a 'make archclean' before './configure'."
-# $Id: configure 14833 2011-12-19 21:57:30Z notin $
+# $Id: configure 15089 2012-03-26 16:41:59Z notin $
diff --git a/ide/coq.ml b/ide/coq.ml
index 1c6229b4..1a5b9def 100644
--- a/ide/coq.ml
+++ b/ide/coq.ml
@@ -6,7 +6,7 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(* $Id: coq.ml 14641 2011-11-06 11:59:10Z herbelin $ *)
+(* $Id: coq.ml 15025 2012-03-09 14:27:07Z glondu $ *)
open Vernac
open Vernacexpr
@@ -112,7 +112,7 @@ let is_in_proof_mode () =
| _ -> true
let user_error_loc l s =
- raise (Stdpp.Exc_located (l, Util.UserError ("CoqIde", s)))
+ raise (Compat.Exc_located (l, Util.UserError ("CoqIde", s)))
type printing_state = {
mutable printing_implicit : bool;
@@ -443,7 +443,7 @@ let interp_and_replace s =
let rec is_pervasive_exn = function
| Out_of_memory | Stack_overflow | Sys.Break -> true
| Error_in_file (_,_,e) -> is_pervasive_exn e
- | Stdpp.Exc_located (_,e) -> is_pervasive_exn e
+ | Compat.Exc_located (_,e) -> is_pervasive_exn e
| DuringCommandInterp (_,e) -> is_pervasive_exn e
| _ -> false
@@ -456,7 +456,7 @@ let print_toplevel_error exc =
in
let (loc,exc) =
match exc with
- | Stdpp.Exc_located (loc, ie) -> (Some loc),ie
+ | Compat.Exc_located (loc, ie) -> (Some loc),ie
| Error_in_file (s, (_,fname, loc), ie) -> None, ie
| _ -> dloc,exc
in
diff --git a/ide/coqide.ml b/ide/coqide.ml
index 162728ad..0c99b8a2 100644
--- a/ide/coqide.ml
+++ b/ide/coqide.ml
@@ -6,7 +6,7 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(* $Id: coqide.ml 14641 2011-11-06 11:59:10Z herbelin $ *)
+(* $Id: coqide.ml 15023 2012-03-08 22:35:31Z pboutill $ *)
open Preferences
open Vernacexpr
@@ -1267,14 +1267,14 @@ object(self)
| l when List.mem `MOD1 l ->
let k = GdkEvent.Key.keyval k in
if GdkKeysyms._Return=k
- then ignore(
+ then let _ =
if (input_buffer#insert_interactive "\n") then
begin
let i= self#get_insert#backward_word_start in
prerr_endline "active_kp_hf: Placing cursor";
self#process_until_iter_or_error i
- end);
- true
+ end in
+ true else false
| l when List.mem `CONTROL l ->
let k = GdkEvent.Key.keyval k in
if GdkKeysyms._Break=k
diff --git a/interp/constrintern.ml b/interp/constrintern.ml
index 4310a01e..96393659 100644
--- a/interp/constrintern.ml
+++ b/interp/constrintern.ml
@@ -6,7 +6,7 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(* $Id: constrintern.ml 14656 2011-11-16 08:46:31Z herbelin $ *)
+(* $Id: constrintern.ml 15072 2012-03-20 17:36:33Z herbelin $ *)
open Pp
open Util
@@ -693,8 +693,9 @@ let apply_scope_env (ids,unb,_,scopes) = function
| [] -> (ids,unb,None,scopes), []
| sc::scl -> (ids,unb,sc,scopes), scl
-let rec simple_adjust_scopes n = function
- | [] -> if n=0 then [] else None :: simple_adjust_scopes (n-1) []
+let rec simple_adjust_scopes n scopes =
+ if n=0 then [] else match scopes with
+ | [] -> None :: simple_adjust_scopes (n-1) []
| sc::scopes -> sc :: simple_adjust_scopes (n-1) scopes
let find_remaining_constructor_scopes pl1 pl2 (ind,j as cstr) =
@@ -771,9 +772,6 @@ let message_redundant_alias (id1,id2) =
(* Expanding notations *)
-let error_invalid_pattern_notation loc =
- user_err_loc (loc,"",str "Invalid notation for pattern.")
-
let chop_aconstr_constructor loc (ind,k) args =
if List.length args = 0 then (* Tolerance for a @id notation *) args else
begin
diff --git a/interp/notation.ml b/interp/notation.ml
index 6e02c40b..4b67f8bd 100644
--- a/interp/notation.ml
+++ b/interp/notation.ml
@@ -6,7 +6,7 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(* $Id: notation.ml 14820 2011-12-18 22:11:32Z herbelin $ *)
+(* $Id: notation.ml 14882 2012-01-05 23:44:40Z herbelin $ *)
(*i*)
open Util
diff --git a/interp/topconstr.ml b/interp/topconstr.ml
index 2d4e41ec..bcd07aea 100644
--- a/interp/topconstr.ml
+++ b/interp/topconstr.ml
@@ -6,7 +6,7 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(* $Id: topconstr.ml 14641 2011-11-06 11:59:10Z herbelin $ *)
+(* $Id: topconstr.ml 15072 2012-03-20 17:36:33Z herbelin $ *)
(*i*)
open Pp
@@ -903,6 +903,12 @@ let names_of_local_binders bl =
List.flatten (List.map (function LocalRawAssum(l,_,_)->l|LocalRawDef(l,_)->[l]) bl)
(**********************************************************************)
+(* Miscellaneous *)
+
+let error_invalid_pattern_notation loc =
+ user_err_loc (loc,"",str "Invalid notation for pattern.")
+
+(**********************************************************************)
(* Functions on constr_expr *)
let constr_loc = function
diff --git a/interp/topconstr.mli b/interp/topconstr.mli
index ce9de27b..abfbd9a1 100644
--- a/interp/topconstr.mli
+++ b/interp/topconstr.mli
@@ -6,7 +6,7 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(*i $Id: topconstr.mli 14641 2011-11-06 11:59:10Z herbelin $ i*)
+(*i $Id: topconstr.mli 15072 2012-03-20 17:36:33Z herbelin $ i*)
(*i*)
open Pp
@@ -282,3 +282,7 @@ val ntn_loc :
Util.loc -> constr_notation_substitution -> string -> (int * int) list
val patntn_loc :
Util.loc -> cases_pattern_notation_substitution -> string -> (int * int) list
+
+(** For cases pattern parsing errors *)
+
+val error_invalid_pattern_notation : Util.loc -> 'a
diff --git a/kernel/term.mli b/kernel/term.mli
index c9a97bbe..69828715 100644
--- a/kernel/term.mli
+++ b/kernel/term.mli
@@ -6,7 +6,7 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(*i $Id: term.mli 14641 2011-11-06 11:59:10Z herbelin $ i*)
+(*i $Id: term.mli 15029 2012-03-13 14:47:00Z herbelin $ i*)
(*i*)
open Names
@@ -406,8 +406,7 @@ val it_mkProd_or_LetIn : types -> rel_context -> types
(*s Other term destructors. *)
(* Transforms a product term $(x_1:T_1)..(x_n:T_n)T$ into the pair
- $([(x_n,T_n);...;(x_1,T_1)],T)$, where $T$ is not a product.
- It includes also local definitions *)
+ $([(x_n,T_n);...;(x_1,T_1)],T)$, where $T$ is not a product. *)
val decompose_prod : constr -> (name*constr) list * constr
(* Transforms a lambda term $[x_1:T_1]..[x_n:T_n]T$ into the pair
diff --git a/kernel/univ.ml b/kernel/univ.ml
index 0646a501..869a60e2 100644
--- a/kernel/univ.ml
+++ b/kernel/univ.ml
@@ -6,7 +6,7 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(* $Id: univ.ml 14641 2011-11-06 11:59:10Z herbelin $ *)
+(* $Id: univ.ml 15019 2012-03-02 17:27:18Z letouzey $ *)
(* Initial Caml version originates from CoC 4.8 [Dec 1988] *)
(* Extension with algebraic universes by HH [Sep 2001] *)
@@ -234,48 +234,66 @@ type order = EQ | LT | LE | NLE
(** [compare_neq] : is [arcv] in the transitive upward closure of [arcu] ?
- We try to avoid visiting unneeded parts of this transitive closure,
- by stopping as soon as [arcv] is encountered. During the recursive
- traversal, [lt_done] and [le_done] are universes we have already
- visited, they do not contain [arcv]. The 3rd arg is
- [(lt_todo,le_todo)], two lists of universes not yet considered,
- known to be above [arcu], strictly or not.
+ In [strict] mode, we fully distinguish between LE and LT, while in
+ non-strict mode, we simply answer LE for both situations.
+
+ If [arcv] is encountered in a LT part, we could directly answer
+ without visiting unneeded parts of this transitive closure.
+ In [strict] mode, if [arcv] is encountered in a LE part, we could only
+ change the default answer (1st arg [c]) from NLE to LE, since a strict
+ constraint may appear later. During the recursive traversal,
+ [lt_done] and [le_done] are universes we have already visited,
+ they do not contain [arcv]. The 4rd arg is [(lt_todo,le_todo)],
+ two lists of universes not yet considered, known to be above [arcu],
+ strictly or not.
We use depth-first search, but the presence of [arcv] in [new_lt]
is checked as soon as possible : this seems to be slightly faster
on a test.
*)
-let compare_neq g arcu arcv =
- let rec cmp lt_done le_done = function
- | [],[] -> NLE
+let compare_neq strict g arcu arcv =
+ let rec cmp c lt_done le_done = function
+ | [],[] -> c
| arc::lt_todo, le_todo ->
if List.memq arc lt_done then
- cmp lt_done le_done (lt_todo,le_todo)
+ cmp c lt_done le_done (lt_todo,le_todo)
else
let lt_new = can g (arc.lt@arc.le) in
- if List.memq arcv lt_new then LT
- else cmp (arc::lt_done) le_done (lt_new@lt_todo,le_todo)
+ if List.memq arcv lt_new then
+ if strict then LT else LE
+ else cmp c (arc::lt_done) le_done (lt_new@lt_todo,le_todo)
| [], arc::le_todo ->
- if arc == arcv then LE
- (* No need to continue inspecting universes above arc:
- if arcv is strictly above arc, then we would have a cycle *)
+ if arc == arcv then
+ (* No need to continue inspecting universes above arc:
+ if arcv is strictly above arc, then we would have a cycle.
+ But we cannot answer LE yet, a stronger constraint may
+ come later from [le_todo]. *)
+ if strict then cmp LE lt_done le_done ([],le_todo) else LE
else
if (List.memq arc lt_done) || (List.memq arc le_done) then
- cmp lt_done le_done ([],le_todo)
+ cmp c lt_done le_done ([],le_todo)
else
let lt_new = can g arc.lt in
- if List.memq arcv lt_new then LT
+ if List.memq arcv lt_new then
+ if strict then LT else LE
else
let le_new = can g arc.le in
- cmp lt_done (arc::le_done) (lt_new, le_new@le_todo)
+ cmp c lt_done (arc::le_done) (lt_new, le_new@le_todo)
in
- cmp [] [] ([],[arcu])
+ cmp NLE [] [] ([],[arcu])
let compare g u v =
let arcu = repr g u
and arcv = repr g v in
- if arcu == arcv then EQ else compare_neq g arcu arcv
+ if arcu == arcv then EQ else compare_neq true g arcu arcv
+
+let is_leq g u v =
+ let arcu = repr g u
+ and arcv = repr g v in
+ arcu == arcv || (compare_neq false g arcu arcv = LE)
+
+let is_lt g u v = (compare g u v = LT)
(* Invariants : compare(u,v) = EQ <=> compare(v,u) = EQ
compare(u,v) = LT or LE => compare(v,u) = NLE
@@ -312,11 +330,11 @@ let rec check_eq g u v =
let compare_greater g strict u v =
let g = declare_univ u g in
let g = declare_univ v g in
- if not strict && compare_eq g v Set then true else
- match compare g v u with
- | (EQ|LE) -> not strict
- | LT -> true
- | NLE -> false
+ if strict then
+ is_lt g v u
+ else
+ compare_eq g v Set || is_leq g v u
+
(*
let compare_greater g strict u v =
let b = compare_greater g strict u v in
@@ -340,9 +358,7 @@ let setlt g u v =
enter_arc {arcu with lt=v::arcu.lt} g
(* checks that non-redundant *)
-let setlt_if g u v = match compare g u v with
- | LT -> g
- | _ -> setlt g u v
+let setlt_if g u v = if is_lt g u v then g else setlt g u v
(* setleq : universe_level -> universe_level -> unit *)
(* forces u >= v *)
@@ -352,9 +368,7 @@ let setleq g u v =
(* checks that non-redundant *)
-let setleq_if g u v = match compare g u v with
- | NLE -> setleq g u v
- | _ -> g
+let setleq_if g u v = if is_leq g u v then g else setleq g u v
(* merge : universe_level -> universe_level -> unit *)
(* we assume compare(u,v) = LE *)
@@ -398,14 +412,12 @@ let error_inconsistency o u v = raise (UniverseInconsistency (o,Atom u,Atom v))
let enforce_univ_leq u v g =
let g = declare_univ u g in
let g = declare_univ v g in
- match compare g u v with
- | NLE ->
- (match compare g v u with
- | LT -> error_inconsistency Le u v
- | LE -> merge g v u
- | NLE -> setleq g u v
- | EQ -> anomaly "Univ.compare")
- | _ -> g
+ if is_leq g u v then g
+ else match compare g v u with
+ | LT -> error_inconsistency Le u v
+ | LE -> merge g v u
+ | NLE -> setleq g u v
+ | EQ -> anomaly "Univ.compare"
(* enforc_univ_eq : universe_level -> universe_level -> unit *)
(* enforc_univ_eq u v will force u=v if possible, will fail otherwise *)
@@ -432,9 +444,8 @@ let enforce_univ_lt u v g =
| LE -> setlt g u v
| EQ -> error_inconsistency Lt u v
| NLE ->
- (match compare g v u with
- | NLE -> setlt g u v
- | _ -> error_inconsistency Lt u v)
+ if is_leq g v u then error_inconsistency Lt u v
+ else setlt g u v
(* Constraints and sets of consrtaints. *)
@@ -452,7 +463,13 @@ let enforce_constraint cst g =
module Constraint = Set.Make(
struct
type t = univ_constraint
- let compare = Pervasives.compare
+ let compare (u,c,v) (u',c',v') =
+ let i = Pervasives.compare c c' in
+ if i <> 0 then i
+ else
+ let i' = cmp_univ_level u u' in
+ if i' <> 0 then i'
+ else cmp_univ_level v v'
end)
type constraints = Constraint.t
@@ -557,6 +574,14 @@ let no_upper_constraints u cst =
| Atom u -> Constraint.for_all (fun (u1,_,_) -> u1 <> u) cst
| Max _ -> anomaly "no_upper_constraints"
+(* Is u mentionned in v (or equals to v) ? *)
+
+let univ_depends u v =
+ match u, v with
+ | Atom u, Atom v -> u = v
+ | Atom u, Max (gel,gtl) -> List.mem u gel || List.mem u gtl
+ | _ -> anomaly "univ_depends given a non-atomic 1st arg"
+
(* Pretty-printing *)
let num_universes g =
diff --git a/kernel/univ.mli b/kernel/univ.mli
index 4cb6dec1..89b20de3 100644
--- a/kernel/univ.mli
+++ b/kernel/univ.mli
@@ -6,7 +6,7 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(*i $Id: univ.mli 14641 2011-11-06 11:59:10Z herbelin $ i*)
+(*i $Id: univ.mli 15019 2012-03-02 17:27:18Z letouzey $ i*)
(* Universes. *)
@@ -78,6 +78,10 @@ val subst_large_constraints :
val no_upper_constraints : universe -> constraints -> bool
+(** Is u mentionned in v (or equals to v) ? *)
+
+val univ_depends : universe -> universe -> bool
+
(*s Pretty-printing of universes. *)
val pr_uni : universe -> Pp.std_ppcmds
diff --git a/lib/compat.ml4 b/lib/compat.ml4
index 096320ed..a0264dc7 100644
--- a/lib/compat.ml4
+++ b/lib/compat.ml4
@@ -15,6 +15,7 @@ IFDEF OCAML309 THEN DEFINE OCAML308 END
IFDEF CAMLP5 THEN
module M = struct
type loc = Stdpp.location
+exception Exc_located = Ploc.Exc
let dummy_loc = Stdpp.dummy_loc
let make_loc = Stdpp.make_loc
let unloc loc = Stdpp.first_pos loc, Stdpp.last_pos loc
@@ -26,6 +27,7 @@ type lexer = token Token.glexer
end
ELSE IFDEF OCAML308 THEN
module M = struct
+exception Exc_located = Stdpp.Exc_located
type loc = Token.flocation
let dummy_loc = Token.dummy_loc
let make_loc loc = Token.make_loc loc
@@ -45,6 +47,7 @@ type lexer = Token.lexer
end
ELSE
module M = struct
+exception Exc_located = Stdpp.Exc_located
type loc = int * int
let dummy_loc = (0,0)
let make_loc x = x
@@ -59,6 +62,7 @@ END
END
type loc = M.loc
+exception Exc_located = M.Exc_located
let dummy_loc = M.dummy_loc
let make_loc = M.make_loc
let unloc = M.unloc
diff --git a/library/impargs.ml b/library/impargs.ml
index 1c2b5afe..96209505 100644
--- a/library/impargs.ml
+++ b/library/impargs.ml
@@ -6,7 +6,7 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(* $Id: impargs.ml 14641 2011-11-06 11:59:10Z herbelin $ *)
+(* $Id: impargs.ml 15069 2012-03-20 14:06:07Z herbelin $ *)
open Util
open Names
@@ -209,11 +209,10 @@ let rec is_rigid_head t = match kind_of_term t with
(* calcule la liste des arguments implicites *)
-let find_displayed_name_in all avoid na b =
- if all then
- compute_and_force_displayed_name_in (RenamingElsewhereFor b) avoid na b
- else
- compute_displayed_name_in (RenamingElsewhereFor b) avoid na b
+let find_displayed_name_in all avoid na (_,b as envnames_b) =
+ let flag = RenamingElsewhereFor envnames_b in
+ if all then compute_and_force_displayed_name_in flag avoid na b
+ else compute_displayed_name_in flag avoid na b
let compute_implicits_gen strict strongly_strict revpat contextual all env t =
let rigid = ref true in
@@ -221,7 +220,7 @@ let compute_implicits_gen strict strongly_strict revpat contextual all env t =
let t = whd_betadeltaiota env t in
match kind_of_term t with
| Prod (na,a,b) ->
- let na',avoid' = find_displayed_name_in all avoid na b in
+ let na',avoid' = find_displayed_name_in all avoid na (names,b) in
add_free_rels_until strict strongly_strict revpat n env a (Hyp (n+1))
(aux (push_rel (na',None,a) env) avoid' (n+1) (na'::names) b)
| _ ->
@@ -234,7 +233,7 @@ let compute_implicits_gen strict strongly_strict revpat contextual all env t =
in
match kind_of_term (whd_betadeltaiota env t) with
| Prod (na,a,b) ->
- let na',avoid = find_displayed_name_in all [] na b in
+ let na',avoid = find_displayed_name_in all [] na ([],b) in
let v = aux (push_rel (na',None,a) env) avoid 1 [na'] b in
!rigid, Array.to_list v
| _ -> true, []
diff --git a/man/coqtop.1 b/man/coqtop.1
index a3b3aac4..3eab597f 100644
--- a/man/coqtop.1
+++ b/man/coqtop.1
@@ -53,7 +53,7 @@ read state from file
.TP
.B \-nois
-start with an empty intial state
+start with an empty initial state
.TP
.BI \-outputstate filename
diff --git a/parsing/egrammar.ml b/parsing/egrammar.ml
index ba965a54..072b09fa 100644
--- a/parsing/egrammar.ml
+++ b/parsing/egrammar.ml
@@ -6,7 +6,7 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(* $Id: egrammar.ml 14779 2011-12-07 21:54:18Z herbelin $ *)
+(* $Id: egrammar.ml 15072 2012-03-20 17:36:33Z herbelin $ *)
open Pp
open Util
@@ -109,11 +109,14 @@ let make_constr_action
in
make ([],[],[]) (List.rev pil)
+let check_cases_pattern_env loc (env,envlist,hasbinders) =
+ if hasbinders then error_invalid_pattern_notation loc else (env,envlist)
+
let make_cases_pattern_action
(f : loc -> cases_pattern_notation_substitution -> cases_pattern_expr) pil =
- let rec make (env,envlist as fullenv) = function
+ let rec make (env,envlist,hasbinders as fullenv) = function
| [] ->
- Gramext.action (fun loc -> f loc fullenv)
+ Gramext.action (fun loc -> f loc (check_cases_pattern_env loc fullenv))
| (GramConstrTerminal _ | GramConstrNonTerminal (_,None)) :: tl ->
(* parse a non-binding item *)
Gramext.action (fun _ -> make fullenv tl)
@@ -121,28 +124,37 @@ let make_cases_pattern_action
(* parse a binding non-terminal *)
(match typ with
| ETConstr _ -> (* pattern non-terminal *)
- Gramext.action (fun (v:cases_pattern_expr) -> make (v::env,envlist) tl)
+ Gramext.action (fun (v:cases_pattern_expr) ->
+ make (v::env, envlist, hasbinders) tl)
| ETReference ->
Gramext.action (fun (v:reference) ->
- make (CPatAtom (dummy_loc,Some v) :: env, envlist) tl)
+ make (CPatAtom (dummy_loc,Some v) :: env, envlist, hasbinders) tl)
| ETName ->
Gramext.action (fun (na:name located) ->
- make (cases_pattern_expr_of_name na :: env, envlist) tl)
+ make (cases_pattern_expr_of_name na :: env, envlist, hasbinders) tl)
| ETBigint ->
Gramext.action (fun (v:Bigint.bigint) ->
- make (CPatPrim (dummy_loc,Numeral v) :: env, envlist) tl)
+ make (CPatPrim (dummy_loc,Numeral v) :: env, envlist, hasbinders) tl)
| ETConstrList (_,_) ->
Gramext.action (fun (vl:cases_pattern_expr list) ->
- make (env, vl :: envlist) tl)
- | (ETPattern | ETBinderList _ | ETBinder _ | ETOther _) ->
- failwith "Unexpected entry of type cases pattern or other")
+ make (env, vl :: envlist, hasbinders) tl)
+ | ETBinder _ | ETBinderList (true,_) ->
+ Gramext.action (fun (v:local_binder list) ->
+ make (env, envlist, hasbinders) tl)
+ | ETBinderList (false,_) ->
+ Gramext.action (fun (v:local_binder list list) ->
+ make (env, envlist, true) tl)
+ | (ETPattern | ETOther _) ->
+ anomaly "Unexpected entry of type cases pattern or other")
| GramConstrListMark (n,b) :: tl ->
(* Rebuild expansions of ConstrList *)
let heads,env = list_chop n env in
- if b then make (env,(heads@List.hd envlist)::List.tl envlist) tl
- else make (env,heads::envlist) tl
+ if b then
+ make (env,(heads@List.hd envlist)::List.tl envlist,hasbinders) tl
+ else
+ make (env,heads::envlist,hasbinders) tl
in
- make ([],[]) (List.rev pil)
+ make ([],[],false) (List.rev pil)
let rec make_constr_prod_item assoc from forpat = function
| GramConstrTerminal tok :: l ->
diff --git a/parsing/ppvernac.ml b/parsing/ppvernac.ml
index 44ac445d..3ed4d8a7 100644
--- a/parsing/ppvernac.ml
+++ b/parsing/ppvernac.ml
@@ -6,7 +6,7 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(* $Id: ppvernac.ml 14657 2011-11-16 08:46:33Z herbelin $ *)
+(* $Id: ppvernac.ml 15025 2012-03-09 14:27:07Z glondu $ *)
open Pp
open Names
@@ -781,7 +781,7 @@ let rec pr_vernac = function
(if i = 1 then mt() else int i ++ str ": ") ++
pr_raw_tactic tac
++ (try if deftac & Pfedit.get_end_tac() <> None then str ".." else mt ()
- with UserError _|Stdpp.Exc_located _ -> mt())
+ with UserError _|Compat.Exc_located _ -> mt())
| VernacSolveExistential (i,c) ->
str"Existential " ++ int i ++ pr_lconstrarg c
diff --git a/parsing/tacextend.ml4 b/parsing/tacextend.ml4
index 0d7a9cfe..2fbe3f44 100644
--- a/parsing/tacextend.ml4
+++ b/parsing/tacextend.ml4
@@ -8,7 +8,7 @@
(*i camlp4use: "pa_extend.cmo q_MLast.cmo" i*)
-(* $Id: tacextend.ml4 14641 2011-11-06 11:59:10Z herbelin $ *)
+(* $Id: tacextend.ml4 15043 2012-03-18 13:57:01Z herbelin $ *)
open Util
open Genarg
@@ -131,19 +131,27 @@ let make_one_printing_rule se (pt,e) =
let make_printing_rule se = mlexpr_of_list (make_one_printing_rule se)
-let rec contains_epsilon = function
- | List0ArgType _ -> true
- | List1ArgType t -> contains_epsilon t
- | OptArgType _ -> true
- | PairArgType(t1,t2) -> contains_epsilon t1 && contains_epsilon t2
- | ExtraArgType("hintbases") -> true
- | _ -> false
-let is_atomic = function
- | GramTerminal s :: l when
- List.for_all (function
- GramTerminal _ -> false
- | GramNonTerminal(_,t,_,_) -> contains_epsilon t) l
- -> [s]
+let rec contains_epsilon loc = function
+ | List0ArgType _ as t ->
+ <:expr< Genarg.in_gen $make_globwit loc t$ [] >>
+ | List1ArgType t' as t ->
+ <:expr< Genarg.in_gen $make_globwit loc t$
+ [out_gen $make_globwit loc t'$ $contains_epsilon loc t'$] >>
+ | OptArgType _ as t ->
+ <:expr< Genarg.in_gen $make_globwit loc t$ None >>
+(* | PairArgType(t1,t2) -> contains_epsilon t1 && contains_epsilon t2*)
+ | ExtraArgType("hintbases") as t ->
+ <:expr< Genarg.in_gen $make_globwit loc t$ (Some []) >> (* fragile *)
+ | _ -> raise Exit
+
+let is_atomic loc = function
+ | GramTerminal s :: l ->
+ (try
+ let l = List.map (function
+ GramTerminal _ -> raise Exit
+ | GramNonTerminal(_,t,_,_) -> contains_epsilon loc t) l
+ in [<:expr< ($str:s$, $mlexpr_of_list (fun x -> x) l$) >>]
+ with Exit -> [])
| _ -> []
let declare_tactic loc s cl =
@@ -163,8 +171,8 @@ let declare_tactic loc s cl =
in
let hidden = if List.length cl = 1 then List.map hide_tac cl else [] in
let atomic_tactics =
- mlexpr_of_list mlexpr_of_string
- (List.flatten (List.map (fun (al,_) -> is_atomic al) cl)) in
+ mlexpr_of_list (fun x -> x)
+ (List.flatten (List.map (fun (al,_) -> is_atomic loc al) cl)) in
<:str_item<
declare
open Pcoq;
@@ -173,9 +181,9 @@ let declare_tactic loc s cl =
try
let _=Tacinterp.add_tactic $se$ (fun [ $list:make_clauses s cl$ ]) in
List.iter
- (fun s -> Tacinterp.add_primitive_tactic s
+ (fun (s,l) -> Tacinterp.add_primitive_tactic s
(Tacexpr.TacAtom($default_loc$,
- Tacexpr.TacExtend($default_loc$,s,[]))))
+ Tacexpr.TacExtend($default_loc$,$se$,l))))
$atomic_tactics$
with e -> Pp.pp (Cerrors.explain_exn e);
Egrammar.extend_tactic_grammar $se$ $gl$;
diff --git a/plugins/funind/recdef.ml b/plugins/funind/recdef.ml
index 83868da9..934bf683 100644
--- a/plugins/funind/recdef.ml
+++ b/plugins/funind/recdef.ml
@@ -8,7 +8,7 @@
(*i camlp4deps: "parsing/grammar.cma" i*)
-(* $Id: recdef.ml 14641 2011-11-06 11:59:10Z herbelin $ *)
+(* $Id: recdef.ml 15069 2012-03-20 14:06:07Z herbelin $ *)
open Term
open Termops
@@ -51,7 +51,8 @@ open Genarg
let compute_renamed_type gls c =
- rename_bound_vars_as_displayed [] (pf_type_of gls c)
+ rename_bound_vars_as_displayed (*no avoid*) [] (*no rels*) []
+ (pf_type_of gls c)
let qed () = Lemmas.save_named true
let defined () = Lemmas.save_named false
diff --git a/plugins/romega/ReflOmegaCore.v b/plugins/romega/ReflOmegaCore.v
index c82abfc8..04eac3a8 100644
--- a/plugins/romega/ReflOmegaCore.v
+++ b/plugins/romega/ReflOmegaCore.v
@@ -872,7 +872,7 @@ Arguments Scope Tint [Int_scope].
Arguments Scope Tplus [romega_scope romega_scope].
Arguments Scope Tmult [romega_scope romega_scope].
Arguments Scope Tminus [romega_scope romega_scope].
-Arguments Scope Topp [romega_scope romega_scope].
+Arguments Scope Topp [romega_scope].
Infix "+" := Tplus : romega_scope.
Infix "*" := Tmult : romega_scope.
diff --git a/plugins/subtac/subtac_obligations.ml b/plugins/subtac/subtac_obligations.ml
index d3a63410..80e712e5 100644
--- a/plugins/subtac/subtac_obligations.ml
+++ b/plugins/subtac/subtac_obligations.ml
@@ -485,8 +485,8 @@ and solve_obligation_by_tac prg obls i tac =
true
else false
with
- | Stdpp.Exc_located(_, Proof_type.LtacLocated (_, Refiner.FailError (_, s)))
- | Stdpp.Exc_located(_, Refiner.FailError (_, s))
+ | Compat.Exc_located(_, Proof_type.LtacLocated (_, Refiner.FailError (_, s)))
+ | Compat.Exc_located(_, Refiner.FailError (_, s))
| Refiner.FailError (_, s) ->
user_err_loc (fst obl.obl_source, "solve_obligation", Lazy.force s)
| e -> false
diff --git a/pretyping/cases.ml b/pretyping/cases.ml
index 749101f7..4205f517 100644
--- a/pretyping/cases.ml
+++ b/pretyping/cases.ml
@@ -6,7 +6,7 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(* $Id: cases.ml 14675 2011-11-17 22:19:34Z herbelin $ *)
+(* $Id: cases.ml 15025 2012-03-09 14:27:07Z glondu $ *)
open Util
open Names
@@ -100,7 +100,7 @@ let rec list_try_compile f = function
| h::t ->
try f h
with UserError _ | TypeError _ | PretypeError _
- | Stdpp.Exc_located (_,(UserError _ | TypeError _ | PretypeError _)) ->
+ | Compat.Exc_located (_,(UserError _ | TypeError _ | PretypeError _)) ->
list_try_compile f t
let force_name =
diff --git a/pretyping/clenv.ml b/pretyping/clenv.ml
index abfef8d4..c2dd9f03 100644
--- a/pretyping/clenv.ml
+++ b/pretyping/clenv.ml
@@ -6,7 +6,7 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(* $Id: clenv.ml 14641 2011-11-06 11:59:10Z herbelin $ *)
+(* $Id: clenv.ml 15069 2012-03-20 14:06:07Z herbelin $ *)
open Pp
open Util
@@ -146,9 +146,6 @@ let mk_clenv_from_n gls n (c,cty) =
let mk_clenv_from gls = mk_clenv_from_n gls None
-let mk_clenv_rename_from_n gls n (c,t) =
- mk_clenv_from_n gls n (c,rename_bound_vars_as_displayed [] t)
-
let mk_clenv_type_of gls t = mk_clenv_from gls (t,pf_type_of gls t)
(******************************************************************)
@@ -460,8 +457,8 @@ let make_clenv_binding_gen hyps_only n env sigma (c,t) = function
let clause = mk_clenv_from_env env sigma n (c,t) in
clenv_constrain_dep_args hyps_only largs clause
| ExplicitBindings lbind ->
- let clause = mk_clenv_from_env env sigma n
- (c,rename_bound_vars_as_displayed [] t)
+ let clause = mk_clenv_from_env env sigma n
+ (c,rename_bound_vars_as_displayed [] [] t)
in clenv_match_args lbind clause
| NoBindings ->
mk_clenv_from_env env sigma n (c,t)
diff --git a/pretyping/detyping.ml b/pretyping/detyping.ml
index 14e72807..fe4354b6 100644
--- a/pretyping/detyping.ml
+++ b/pretyping/detyping.ml
@@ -6,7 +6,7 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(* $Id: detyping.ml 14641 2011-11-06 11:59:10Z herbelin $ *)
+(* $Id: detyping.ml 15069 2012-03-20 14:06:07Z herbelin $ *)
open Pp
open Util
@@ -533,7 +533,7 @@ and detype_eqn isgoal avoid env constr construct_nargs branch =
buildrec [] [] avoid env construct_nargs branch
and detype_binder isgoal bk avoid env na ty c =
- let flag = if isgoal then RenamingForGoal else (RenamingElsewhereFor c) in
+ let flag = if isgoal then RenamingForGoal else RenamingElsewhereFor (env,c) in
let na',avoid' =
if bk = BLetIn then compute_displayed_let_name_in flag avoid na c
else compute_displayed_name_in flag avoid na c in
@@ -553,9 +553,11 @@ let rec detype_rel_context where avoid env sign =
| None -> na,avoid
| Some c ->
if b<>None then
- compute_displayed_let_name_in (RenamingElsewhereFor c) avoid na c
+ compute_displayed_let_name_in
+ (RenamingElsewhereFor (env,c)) avoid na c
else
- compute_displayed_name_in (RenamingElsewhereFor c) avoid na c in
+ compute_displayed_name_in
+ (RenamingElsewhereFor (env,c)) avoid na c in
let b = Option.map (detype false avoid env) b in
let t = detype false avoid env t in
(na',Explicit,b,t) :: aux avoid' (add_name na' env) rest
diff --git a/pretyping/inductiveops.ml b/pretyping/inductiveops.ml
index 6e54c170..fe90941d 100644
--- a/pretyping/inductiveops.ml
+++ b/pretyping/inductiveops.ml
@@ -6,7 +6,7 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(* $Id: inductiveops.ml 14641 2011-11-06 11:59:10Z herbelin $ *)
+(* $Id: inductiveops.ml 15019 2012-03-02 17:27:18Z letouzey $ *)
open Util
open Names
@@ -403,21 +403,6 @@ let arity_of_case_predicate env (ind,params) dep k =
(* Inferring the sort of parameters of a polymorphic inductive type
knowing the sort of the conclusion *)
-(* Check if u (sort of a parameter) appears in the sort of the
- inductive (is). This is done by trying to enforce u > u' >= is
- in the empty univ graph. If an inconsistency appears, then
- is depends on u. *)
-let is_constrained is u =
- try
- let u' = fresh_local_univ() in
- let _ =
- merge_constraints
- (enforce_geq u (super u')
- (enforce_geq u' is Constraint.empty))
- initial_universes in
- false
- with UniverseInconsistency _ -> true
-
(* Compute the inductive argument types: replace the sorts
that appear in the type of the inductive by the sort of the
conclusion, and the other ones by fresh universes. *)
@@ -429,7 +414,9 @@ let rec instantiate_universes env scl is = function
| (na,None,ty)::sign, Some u::exp ->
let ctx,_ = Reduction.dest_arity env ty in
let s =
- if is_constrained is u then
+ (* Does the sort of parameter [u] appear in (or equal)
+ the sort of inductive [is] ? *)
+ if univ_depends u is then
scl (* constrained sort: replace by scl *)
else
(* unconstriained sort: replace by fresh universe *)
diff --git a/pretyping/namegen.ml b/pretyping/namegen.ml
index 45060511..f133d842 100644
--- a/pretyping/namegen.ml
+++ b/pretyping/namegen.ml
@@ -6,7 +6,7 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(* $Id: namegen.ml 14641 2011-11-06 11:59:10Z herbelin $ *)
+(* $Id: namegen.ml 15069 2012-03-20 14:06:07Z herbelin $ *)
(* Created from contents that was formerly in termops.ml and
nameops.ml, Nov 2009 *)
@@ -223,22 +223,27 @@ let make_all_name_different env =
looks for name of same base with lower available subscript beyond current
subscript *)
-let visibly_occur_id id c =
- let rec occur c = match kind_of_term c with
+let occur_rel p env id =
+ try lookup_name_of_rel p env = Name id
+ with Not_found -> false (* Unbound indice : may happen in debug *)
+
+let visibly_occur_id id (nenv,c) =
+ let rec occur n c = match kind_of_term c with
| Const _ | Ind _ | Construct _ | Var _
when shortest_qualid_of_global Idset.empty (global_of_constr c)
= qualid_of_ident id -> raise Occur
- | _ -> iter_constr occur c
+ | Rel p when p>n & occur_rel (p-n) nenv id -> raise Occur
+ | _ -> iter_constr_with_binders succ occur n c
in
- try occur c; false
+ try occur 1 c; false
with Occur -> true
| Not_found -> false (* Happens when a global is not in the env *)
-let next_ident_away_for_default_printing t id avoid =
- let bad id = List.mem id avoid or visibly_occur_id id t in
+let next_ident_away_for_default_printing env_t id avoid =
+ let bad id = List.mem id avoid or visibly_occur_id id env_t in
next_ident_away_from id bad
-let next_name_away_for_default_printing t na avoid =
+let next_name_away_for_default_printing env_t na avoid =
let id = match na with
| Name id -> id
| Anonymous ->
@@ -246,7 +251,7 @@ let next_name_away_for_default_printing t na avoid =
(* taken into account by the function compute_displayed_name_in; *)
(* just in case, invent a valid name *)
id_of_string "H" in
- next_ident_away_for_default_printing t id avoid
+ next_ident_away_for_default_printing env_t id avoid
(**********************************************************************)
(* Displaying terms avoiding bound variables clashes *)
@@ -269,13 +274,13 @@ let next_name_away_for_default_printing t na avoid =
type renaming_flags =
| RenamingForCasesPattern
| RenamingForGoal
- | RenamingElsewhereFor of constr
+ | RenamingElsewhereFor of (name list * constr)
let next_name_for_display flags =
match flags with
| RenamingForCasesPattern -> next_name_away_in_cases_pattern
| RenamingForGoal -> next_name_away_in_goal
- | RenamingElsewhereFor t -> next_name_away_for_default_printing t
+ | RenamingElsewhereFor env_t -> next_name_away_for_default_printing env_t
(* Remark: Anonymous var may be dependent in Evar's contexts *)
let compute_displayed_name_in flags avoid na c =
@@ -297,16 +302,20 @@ let compute_displayed_let_name_in flags avoid na c =
let fresh_id = next_name_for_display flags na avoid in
(Name fresh_id, fresh_id::avoid)
-let rec rename_bound_vars_as_displayed avoid c =
- let rec rename avoid c =
+let rec rename_bound_vars_as_displayed avoid env c =
+ let rec rename avoid env c =
match kind_of_term c with
| Prod (na,c1,c2) ->
- let na',avoid' = compute_displayed_name_in (RenamingElsewhereFor c2) avoid na c2 in
- mkProd (na', c1, rename avoid' c2)
+ let na',avoid' =
+ compute_displayed_name_in
+ (RenamingElsewhereFor (env,c2)) avoid na c2 in
+ mkProd (na', c1, rename avoid' (add_name na' env) c2)
| LetIn (na,c1,t,c2) ->
- let na',avoid' = compute_displayed_let_name_in (RenamingElsewhereFor c2) avoid na c2 in
- mkLetIn (na',c1,t, rename avoid' c2)
- | Cast (c,k,t) -> mkCast (rename avoid c, k,t)
+ let na',avoid' =
+ compute_displayed_let_name_in
+ (RenamingElsewhereFor (env,c2)) avoid na c2 in
+ mkLetIn (na',c1,t, rename avoid' (add_name na' env) c2)
+ | Cast (c,k,t) -> mkCast (rename avoid env c, k,t)
| _ -> c
in
- rename avoid c
+ rename avoid env c
diff --git a/pretyping/namegen.mli b/pretyping/namegen.mli
index f99ee3f6..464efcf8 100644
--- a/pretyping/namegen.mli
+++ b/pretyping/namegen.mli
@@ -6,7 +6,7 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(* $Id: namegen.mli 14641 2011-11-06 11:59:10Z herbelin $ *)
+(* $Id: namegen.mli 15069 2012-03-20 14:06:07Z herbelin $ *)
open Names
open Term
@@ -64,7 +64,7 @@ val next_name_away_with_default : string -> name -> identifier list ->
type renaming_flags =
| RenamingForCasesPattern (* avoid only global constructors *)
| RenamingForGoal (* avoid all globals (as in intro) *)
- | RenamingElsewhereFor of constr
+ | RenamingElsewhereFor of (name list * constr)
val make_all_name_different : env -> env
@@ -74,4 +74,5 @@ val compute_and_force_displayed_name_in :
renaming_flags -> identifier list -> name -> constr -> name * identifier list
val compute_displayed_let_name_in :
renaming_flags -> identifier list -> name -> constr -> name * identifier list
-val rename_bound_vars_as_displayed : identifier list -> types -> types
+val rename_bound_vars_as_displayed :
+ identifier list -> name list -> types -> types
diff --git a/pretyping/pretype_errors.ml b/pretyping/pretype_errors.ml
index 688a25b9..a9b2a18b 100644
--- a/pretyping/pretype_errors.ml
+++ b/pretyping/pretype_errors.ml
@@ -6,7 +6,7 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(* $Id: pretype_errors.ml 14641 2011-11-06 11:59:10Z herbelin $ *)
+(* $Id: pretype_errors.ml 15025 2012-03-09 14:27:07Z glondu $ *)
open Util
open Stdpp
@@ -45,7 +45,7 @@ exception PretypeError of env * pretype_error
let precatchable_exception = function
| Util.UserError _ | TypeError _ | PretypeError _
- | Stdpp.Exc_located(_,(Util.UserError _ | TypeError _ |
+ | Compat.Exc_located(_,(Util.UserError _ | TypeError _ |
Nametab.GlobalizationError _ | PretypeError _)) -> true
| _ -> false
diff --git a/pretyping/typeclasses_errors.ml b/pretyping/typeclasses_errors.ml
index 62941a76..7b09f957 100644
--- a/pretyping/typeclasses_errors.ml
+++ b/pretyping/typeclasses_errors.ml
@@ -6,7 +6,7 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(*i $Id: typeclasses_errors.ml 14641 2011-11-06 11:59:10Z herbelin $ i*)
+(*i $Id: typeclasses_errors.ml 15025 2012-03-09 14:27:07Z glondu $ i*)
(*i*)
open Names
@@ -47,7 +47,7 @@ let unsatisfiable_constraints env evd ev =
raise (TypeClassError (env, UnsatisfiableConstraints (evd, None)))
| Some ev ->
let loc, kind = Evd.evar_source ev evd in
- raise (Stdpp.Exc_located (loc, TypeClassError
+ raise (Compat.Exc_located (loc, TypeClassError
(env, UnsatisfiableConstraints (evd, Some (ev, kind)))))
let mismatched_ctx_inst env c n m = typeclass_error env (MismatchedContextInstance (c, n, m))
@@ -55,5 +55,5 @@ let mismatched_ctx_inst env c n m = typeclass_error env (MismatchedContextInstan
let rec unsatisfiable_exception exn =
match exn with
| TypeClassError (_, UnsatisfiableConstraints _) -> true
- | Stdpp.Exc_located(_, e) -> unsatisfiable_exception e
+ | Compat.Exc_located(_, e) -> unsatisfiable_exception e
| _ -> false
diff --git a/pretyping/vnorm.ml b/pretyping/vnorm.ml
index 395f5c8d..57b183d5 100644
--- a/pretyping/vnorm.ml
+++ b/pretyping/vnorm.ml
@@ -6,7 +6,7 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(*i $Id: vnorm.ml 14641 2011-11-06 11:59:10Z herbelin $ i*)
+(*i $Id: vnorm.ml 15029 2012-03-13 14:47:00Z herbelin $ i*)
open Names
open Declarations
@@ -111,7 +111,7 @@ let build_branches_type env (mind,_ as _ind) mib mip params dep p =
a 0) et les lambda correspondant aux realargs *)
let build_one_branch i cty =
let typi = type_constructor mind mib cty params in
- let decl,indapp = Term.decompose_prod typi in
+ let decl,indapp = decompose_prod_assum typi in
let ind,cargs = find_rectype_a env indapp in
let nparams = Array.length params in
let carity = snd (rtbl.(i)) in
@@ -195,11 +195,8 @@ and nf_stk env c t stk =
let bsw = branch_of_switch (nb_rel env) sw in
let mkbranch i (n,v) =
let decl,codom = btypes.(i) in
- let env =
- List.fold_right
- (fun (name,t) env -> push_rel (name,None,t) env) decl env in
- let b = nf_val env v codom in
- compose_lam decl b
+ let b = nf_val (push_rel_context decl env) v codom in
+ it_mkLambda_or_LetIn b decl
in
let branchs = Array.mapi mkbranch bsw in
let tcase = build_case_type dep p realargs c in
diff --git a/proofs/logic.ml b/proofs/logic.ml
index d837dca5..90514992 100644
--- a/proofs/logic.ml
+++ b/proofs/logic.ml
@@ -6,7 +6,7 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(* $Id: logic.ml 14641 2011-11-06 11:59:10Z herbelin $ *)
+(* $Id: logic.ml 15025 2012-03-09 14:27:07Z glondu $ *)
open Pp
open Util
@@ -48,7 +48,7 @@ exception RefinerError of refiner_error
open Pretype_errors
let rec catchable_exception = function
- | Stdpp.Exc_located(_,e) -> catchable_exception e
+ | Compat.Exc_located(_,e) -> catchable_exception e
| LtacLocated(_,e) -> catchable_exception e
| Util.UserError _ | TypeError _
| RefinerError _ | Indrec.RecursionSchemeError _
diff --git a/proofs/refiner.ml b/proofs/refiner.ml
index a540eef6..87e7f4ce 100644
--- a/proofs/refiner.ml
+++ b/proofs/refiner.ml
@@ -6,7 +6,7 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(* $Id: refiner.ml 14641 2011-11-06 11:59:10Z herbelin $ *)
+(* $Id: refiner.ml 15025 2012-03-09 14:27:07Z glondu $ *)
open Pp
open Util
@@ -494,15 +494,15 @@ let tclNOTSAMEGOAL (tac : tactic) goal =
let catch_failerror e =
if catchable_exception e then check_for_interrupt ()
else match e with
- | FailError (0,_) | Stdpp.Exc_located(_, FailError (0,_))
- | Stdpp.Exc_located(_, LtacLocated (_,FailError (0,_))) ->
+ | FailError (0,_) | Compat.Exc_located(_, FailError (0,_))
+ | Compat.Exc_located(_, LtacLocated (_,FailError (0,_))) ->
check_for_interrupt ()
| FailError (lvl,s) -> raise (FailError (lvl - 1, s))
- | Stdpp.Exc_located(s,FailError (lvl,s')) ->
- raise (Stdpp.Exc_located(s,FailError (lvl - 1, s')))
- | Stdpp.Exc_located(s,LtacLocated (s'',FailError (lvl,s'))) ->
+ | Compat.Exc_located(s,FailError (lvl,s')) ->
+ raise (Compat.Exc_located(s,FailError (lvl - 1, s')))
+ | Compat.Exc_located(s,LtacLocated (s'',FailError (lvl,s'))) ->
raise
- (Stdpp.Exc_located(s,LtacLocated (s'',FailError (lvl - 1,s'))))
+ (Compat.Exc_located(s,LtacLocated (s'',FailError (lvl - 1,s'))))
| e -> raise e
(* ORELSE0 t1 t2 tries to apply t1 and if it fails, applies t2 *)
diff --git a/tactics/class_tactics.ml4 b/tactics/class_tactics.ml4
index 465d1d80..cf9213dd 100644
--- a/tactics/class_tactics.ml4
+++ b/tactics/class_tactics.ml4
@@ -8,7 +8,7 @@
(*i camlp4deps: "parsing/grammar.cma" i*)
-(* $Id: class_tactics.ml4 14641 2011-11-06 11:59:10Z herbelin $ *)
+(* $Id: class_tactics.ml4 15025 2012-03-09 14:27:07Z glondu $ *)
open Pp
open Util
@@ -219,7 +219,7 @@ let e_possible_resolve db_list local_db gl =
let rec catchable = function
| Refiner.FailError _ -> true
- | Stdpp.Exc_located (_, e) -> catchable e
+ | Compat.Exc_located (_, e) -> catchable e
| e -> Logic.catchable_exception e
let is_dep gl gls =
diff --git a/tactics/extratactics.ml4 b/tactics/extratactics.ml4
index c4a2ef44..c7762c69 100644
--- a/tactics/extratactics.ml4
+++ b/tactics/extratactics.ml4
@@ -8,7 +8,7 @@
(*i camlp4deps: "parsing/grammar.cma" i*)
-(* $Id: extratactics.ml4 14641 2011-11-06 11:59:10Z herbelin $ *)
+(* $Id: extratactics.ml4 15025 2012-03-09 14:27:07Z glondu $ *)
open Pp
open Pcoq
@@ -580,7 +580,7 @@ let hResolve id c occ t gl =
try
Pretyping.Default.understand sigma env t_hole
with
- | Stdpp.Exc_located (loc,Pretype_errors.PretypeError (_, Pretype_errors.UnsolvableImplicit _)) ->
+ | Compat.Exc_located (loc,Pretype_errors.PretypeError (_, Pretype_errors.UnsolvableImplicit _)) ->
resolve_hole (subst_hole_with_term (fst (unloc loc)) c_raw t_hole)
in
let t_constr = resolve_hole (subst_var_with_hole occ id t_raw) in
diff --git a/tactics/rewrite.ml4 b/tactics/rewrite.ml4
index fd3eeeb2..cf5fab0c 100644
--- a/tactics/rewrite.ml4
+++ b/tactics/rewrite.ml4
@@ -1057,7 +1057,7 @@ let cl_rewrite_clause_aux ?(abs=None) strat goal_meta clause gl =
else tclIDTAC
in tclTHENLIST [evartac; rewtac] gl
with
- | Stdpp.Exc_located (_, TypeClassError (env, (UnsatisfiableConstraints _ as e)))
+ | Compat.Exc_located (_, TypeClassError (env, (UnsatisfiableConstraints _ as e)))
| TypeClassError (env, (UnsatisfiableConstraints _ as e)) ->
Refiner.tclFAIL_lazy 0
(lazy (str"setoid rewrite failed: unable to satisfy the rewriting constraints."
diff --git a/tactics/tacinterp.ml b/tactics/tacinterp.ml
index 6a11384b..929f1013 100644
--- a/tactics/tacinterp.ml
+++ b/tactics/tacinterp.ml
@@ -6,7 +6,7 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(* $Id: tacinterp.ml 14677 2011-11-17 22:19:38Z herbelin $ *)
+(* $Id: tacinterp.ml 15025 2012-03-09 14:27:07Z glondu $ *)
open Constrintern
open Closure
@@ -93,15 +93,15 @@ let dloc = dummy_loc
let catch_error call_trace tac g =
if call_trace = [] then tac g else try tac g with
| LtacLocated _ as e -> raise e
- | Stdpp.Exc_located (_,LtacLocated _) as e -> raise e
+ | Compat.Exc_located (_,LtacLocated _) as e -> raise e
| e ->
let (nrep,loc',c),tail = list_sep_last call_trace in
- let loc,e' = match e with Stdpp.Exc_located(loc,e) -> loc,e | _ ->dloc,e in
+ let loc,e' = match e with Compat.Exc_located(loc,e) -> loc,e | _ ->dloc,e in
if tail = [] then
let loc = if loc = dloc then loc' else loc in
- raise (Stdpp.Exc_located(loc,e'))
+ raise (Compat.Exc_located(loc,e'))
else
- raise (Stdpp.Exc_located(loc',LtacLocated((nrep,c,tail,loc),e')))
+ raise (Compat.Exc_located(loc',LtacLocated((nrep,c,tail,loc),e')))
(* Signature for interpretation: val_interp and interpretation functions *)
type interp_sign =
@@ -1979,14 +1979,14 @@ and eval_with_fail ist is_lazy goal tac =
VRTactic (catch_error trace tac goal)
| a -> a)
with
- | FailError (0,s) | Stdpp.Exc_located(_, FailError (0,s))
- | Stdpp.Exc_located(_,LtacLocated (_,FailError (0,s))) ->
+ | FailError (0,s) | Compat.Exc_located(_, FailError (0,s))
+ | Compat.Exc_located(_,LtacLocated (_,FailError (0,s))) ->
raise (Eval_fail (Lazy.force s))
| FailError (lvl,s) -> raise (FailError (lvl - 1, s))
- | Stdpp.Exc_located(s,FailError (lvl,s')) ->
- raise (Stdpp.Exc_located(s,FailError (lvl - 1, s')))
- | Stdpp.Exc_located(s,LtacLocated (s'',FailError (lvl,s'))) ->
- raise (Stdpp.Exc_located(s,LtacLocated (s'',FailError (lvl - 1, s'))))
+ | Compat.Exc_located(s,FailError (lvl,s')) ->
+ raise (Compat.Exc_located(s,FailError (lvl - 1, s')))
+ | Compat.Exc_located(s,LtacLocated (s'',FailError (lvl,s'))) ->
+ raise (Compat.Exc_located(s,LtacLocated (s'',FailError (lvl - 1, s'))))
(* Interprets the clauses of a recursive LetIn *)
and interp_letrec ist gl llc u =
diff --git a/tools/coqdoc/cpretty.mll b/tools/coqdoc/cpretty.mll
index 63850bd5..a2bcb987 100644
--- a/tools/coqdoc/cpretty.mll
+++ b/tools/coqdoc/cpretty.mll
@@ -7,7 +7,7 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(*i $Id: cpretty.mll 14641 2011-11-06 11:59:10Z herbelin $ i*)
+(*i $Id: cpretty.mll 14868 2011-12-26 17:07:24Z herbelin $ i*)
(*s Utility functions for the scanners *)
@@ -309,7 +309,12 @@ let thm_token =
let prf_token =
"Next" space+ "Obligation"
- | "Proof" (space* "." | space+ "with")
+ | "Proof" (space* "." | space+ "with" | space+ "using")
+
+let immediate_prf_token =
+ (* Approximation of a proof term, if not in the prf_token case *)
+ (* To be checked after prf_token *)
+ "Proof" space* [^ '.' 'w' 'u']
let def_token =
"Definition"
@@ -384,7 +389,8 @@ let commands =
| ("Hypothesis" | "Hypotheses")
| "End"
-let end_kw = "Qed" | "Defined" | "Save" | "Admitted" | "Abort"
+let end_kw =
+ immediate_prf_token | "Qed" | "Defined" | "Save" | "Admitted" | "Abort"
let extraction =
"Extraction"
@@ -607,7 +613,7 @@ and coq = parse
| prf_token
{ let eol =
if not !Cdglobals.gallina then
- begin backtrack lexbuf; body_bol lexbuf end
+ begin backtrack lexbuf; body lexbuf end
else
let s = lexeme lexbuf in
let eol =
diff --git a/toplevel/cerrors.ml b/toplevel/cerrors.ml
index 86057b4b..095f50c6 100644
--- a/toplevel/cerrors.ml
+++ b/toplevel/cerrors.ml
@@ -6,7 +6,7 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(* $Id: cerrors.ml 14641 2011-11-06 11:59:10Z herbelin $ *)
+(* $Id: cerrors.ml 15025 2012-03-09 14:27:07Z glondu $ *)
open Pp
open Util
@@ -81,7 +81,7 @@ let rec explain_exn_default_aux anomaly_string report_fn = function
hov 0 (str "Syntax error: Undefined token.")
| Lexer.Error (Bad_token s) ->
hov 0 (str "Syntax error: Bad token" ++ spc () ++ str s ++ str ".")
- | Stdpp.Exc_located (loc,exc) ->
+ | Compat.Exc_located (loc,exc) ->
hov 0 ((if loc = dummy_loc then (mt ())
else (str"At location " ++ print_loc loc ++ str":" ++ fnl ()))
++ explain_exn_default_aux anomaly_string report_fn exc)
@@ -156,8 +156,8 @@ let rec process_vernac_interp_error = function
| Proof_type.LtacLocated (s,exc) ->
EvaluatedError (hov 0 (Himsg.explain_ltac_call_trace s ++ fnl()),
Some (process_vernac_interp_error exc))
- | Stdpp.Exc_located (loc,exc) ->
- Stdpp.Exc_located (loc,process_vernac_interp_error exc)
+ | Compat.Exc_located (loc,exc) ->
+ Compat.Exc_located (loc,process_vernac_interp_error exc)
| exc ->
exc
diff --git a/toplevel/toplevel.ml b/toplevel/toplevel.ml
index 9954ff56..551e5574 100644
--- a/toplevel/toplevel.ml
+++ b/toplevel/toplevel.ml
@@ -6,7 +6,7 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(* $Id: toplevel.ml 14641 2011-11-06 11:59:10Z herbelin $ *)
+(* $Id: toplevel.ml 15025 2012-03-09 14:27:07Z glondu $ *)
open Pp
open Util
@@ -274,7 +274,7 @@ let set_prompt prompt =
let rec is_pervasive_exn = function
| Out_of_memory | Stack_overflow | Sys.Break -> true
| Error_in_file (_,_,e) -> is_pervasive_exn e
- | Stdpp.Exc_located (_,e) -> is_pervasive_exn e
+ | Compat.Exc_located (_,e) -> is_pervasive_exn e
| DuringCommandInterp (_,e) -> is_pervasive_exn e
| _ -> false
@@ -290,7 +290,7 @@ let print_toplevel_error exc =
in
let (locstrm,exc) =
match exc with
- | Stdpp.Exc_located (loc, ie) ->
+ | Compat.Exc_located (loc, ie) ->
if valid_buffer_loc top_buffer dloc loc then
(print_highlight_location top_buffer loc, ie)
else
@@ -325,7 +325,7 @@ let parse_to_dot =
let rec discard_to_dot () =
try
Gram.Entry.parse parse_to_dot top_buffer.tokens
- with Stdpp.Exc_located(_,(Token.Error _|Lexer.Error _)) ->
+ with Compat.Exc_located(_,(Token.Error _|Lexer.Error _)) ->
discard_to_dot()
diff --git a/toplevel/vernac.ml b/toplevel/vernac.ml
index a7aef93f..de732618 100644
--- a/toplevel/vernac.ml
+++ b/toplevel/vernac.ml
@@ -6,7 +6,7 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(* $Id: vernac.ml 14641 2011-11-06 11:59:10Z herbelin $ *)
+(* $Id: vernac.ml 15025 2012-03-09 14:27:07Z glondu $ *)
(* Parsing of vernacular. *)
@@ -41,14 +41,14 @@ let raise_with_file file exc =
match re with
| Error_in_file (_, (b,f,loc), e) when loc <> dummy_loc ->
((b, f, loc), e)
- | Stdpp.Exc_located (loc, e) when loc <> dummy_loc ->
+ | Compat.Exc_located (loc, e) when loc <> dummy_loc ->
((false,file, loc), e)
- | Stdpp.Exc_located (_, e) | e -> ((false,file,cmdloc), e)
+ | Compat.Exc_located (_, e) | e -> ((false,file,cmdloc), e)
in
raise (Error_in_file (file, inner, disable_drop inex))
let real_error = function
- | Stdpp.Exc_located (_, e) -> e
+ | Compat.Exc_located (_, e) -> e
| Error_in_file (_, _, e) -> e
| e -> e
@@ -206,7 +206,9 @@ let rec vernac_com interpfun (loc,com) =
| VernacFail v ->
if not !just_parsing then begin try
- interp v; raise HasNotFailed
+ (* If the command actually works, ignore its effects on the state *)
+ States.with_state_protection
+ (fun v -> interp v; raise HasNotFailed) v
with e -> match real_error e with
| HasNotFailed ->
errorlabstrm "Fail" (str "The command has not failed !")