diff options
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 @@ -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) @@ -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 $ @@ -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 !") |