diff options
60 files changed, 1421 insertions, 292 deletions
@@ -13,6 +13,7 @@ Bugfixes - #4592, #4932: notations sharing recursive patterns or sharing binders made more robust. - #4780: Induction with universe polymorphism on was creating ill-typed terms. +- #3070: fixing "subst" in the presence of a chain of dependencies. Specification language @@ -85,13 +86,25 @@ Tools Changes from V8.5pl2 to V8.5pl3 =============================== + +Critical bugfix +- #4876: Guard checker incompleteness when using primitive projections + +Other bugfixes + - #4780: Induction with universe polymorphism on was creating ill-typed terms. +- #4673: regression in setoid_rewrite, unfolding let-ins for type unification. +- #4754: Regression in setoid_rewrite, allow postponed unification problems to remain. +- #4769: Anomaly with universe polymorphic schemes defined inside sections. +- #3886: Program: duplicate obligations of mutual fixpoints Changes from V8.5pl1 to V8.5pl2 =============================== Critical bugfix - Checksums of .vo files dependencies were not correctly checked. +- Unicode-to-ASCII translation was not injective, leading in a soundness bug in + the native compiler. Other bugfixes @@ -613,6 +626,9 @@ Tactics - Behavior of introduction patterns -> and <- made more uniform (hypothesis is cleared, rewrite in hypotheses and conclusion and erasing the variable when rewriting a variable). +- New experimental option "Set Standard Proposition Elimination Names" + so that case analysis or induction on schemes in Type containing + propositions now produces "H"-based names. - Tactics from plugins are now active only when the corresponding module is imported (source of incompatibilities, solvable by adding an "Import"; in the particular case of Omega, use "Require Import OmegaTactic"). @@ -1151,9 +1167,6 @@ Other tactics clears (resp. reverts) H and all the hypotheses that depend on H. - Ltac's pattern-matching now supports matching metavariables that depend on variables bound upwards in the pattern. -- New experimental option "Set Standard Proposition Elimination Names" - so that case analysis or induction on schemes in Type containing - propositions now produces "H"-based names. Tactic definitions diff --git a/configure.ml b/configure.ml index 63cf138db0..13e1daedc5 100644 --- a/configure.ml +++ b/configure.ml @@ -809,7 +809,8 @@ let strip = (** * md5sum command *) let md5sum = - if arch = "Darwin" || arch = "FreeBSD" then "md5 -q" else "md5sum" + if List.mem arch ["Darwin"; "FreeBSD"; "OpenBSD"] + then "md5 -q" else "md5sum" (** * Documentation : do we have latex, hevea, ... *) diff --git a/dev/doc/changes.txt b/dev/doc/changes.txt index feef80ed35..fcee79e07e 100644 --- a/dev/doc/changes.txt +++ b/dev/doc/changes.txt @@ -248,6 +248,8 @@ define_evar_* mostly used internally in the unification engine. open Proofview.Notations Proofview.Goal.enter { enter = begin fun gl -> ... end } + +- `Tacexpr.TacDynamic(Loc.dummy_loc, Pretyping.constr_in c)` --> `Tacinterp.Value.of_constr c` ========================================= = CHANGES BETWEEN COQ V8.4 AND COQ V8.5 = diff --git a/dev/include b/dev/include index b2eb280d6c..d82fb74f22 100644 --- a/dev/include +++ b/dev/include @@ -25,7 +25,7 @@ #cd ".";; #use "base_include";; -#install_printer (* pp_stdcmds *) pppp;; +#install_printer (* pp_stdcmds *) pp;; #install_printer (* pattern *) pppattern;; #install_printer (* glob_constr *) ppglob_constr;; diff --git a/doc/refman/RefMan-ltac.tex b/doc/refman/RefMan-ltac.tex index 5ba3c308a6..9fbff7181e 100644 --- a/doc/refman/RefMan-ltac.tex +++ b/doc/refman/RefMan-ltac.tex @@ -1277,7 +1277,7 @@ Prints the profile Prints a profile for all tactics that start with {\qstring}. Append a period (.) to the string if you only want exactly that name. \begin{quote} -{\tt Reset Profile}. +{\tt Reset Ltac Profile}. \end{quote} Resets the profile, that is, deletes all accumulated information diff --git a/doc/refman/RefMan-oth.tex b/doc/refman/RefMan-oth.tex index 6a8bda35d6..919e7b5cdc 100644 --- a/doc/refman/RefMan-oth.tex +++ b/doc/refman/RefMan-oth.tex @@ -87,7 +87,7 @@ is restored when the current \emph{section} ends. \item {\tt Global Unset {\rm\sl flag}.\comindex{Global Unset}}\\ This command switches {\rm\sl flag} off. The original state of {\rm\sl flag} is \emph{not} restored at the end of the module. Additionally, -if set in a file, {\rm\sl flag} is switched on when the file is +if set in a file, {\rm\sl flag} is switched off when the file is {\tt Require}-d. \end{Variants} diff --git a/engine/evarutil.ml b/engine/evarutil.ml index b63391913f..bd86f4bd27 100644 --- a/engine/evarutil.ml +++ b/engine/evarutil.ml @@ -290,78 +290,107 @@ let make_pure_subst evi args = * we have the property that u and phi(t) are convertible in env. *) +let csubst_subst (k, s) c = + let rec subst n c = match Constr.kind c with + | Rel m -> + if m <= n then c + else if m - n <= k then Int.Map.find (k - m + n) s + else mkRel (m - k) + | _ -> Constr.map_with_binders succ subst n c + in + if k = 0 then c else subst 0 c + let subst2 subst vsubst c = - substl subst (replace_vars vsubst c) + csubst_subst subst (replace_vars vsubst c) -let push_rel_context_to_named_context env typ = - (* compute the instances relative to the named context and rel_context *) +let next_ident_away id avoid = + let avoid id = Id.Set.mem id avoid in + next_ident_away_from id avoid + +let next_name_away na avoid = + let avoid id = Id.Set.mem id avoid in + let id = match na with Name id -> id | Anonymous -> default_non_dependent_ident in + next_ident_away_from id avoid + +type csubst = int * Constr.t Int.Map.t + +let empty_csubst = (0, Int.Map.empty) + +type ext_named_context = + csubst * (Id.t * Constr.constr) list * + Id.Set.t * Context.Named.t + +let push_var id (n, s) = + let s = Int.Map.add n (mkVar id) s in + (succ n, s) + +let push_rel_decl_to_named_context decl (subst, vsubst, avoid, nc) = let open Context.Named.Declaration in - let ids = List.map get_id (named_context env) in - let inst_vars = List.map mkVar ids in - let inst_rels = List.rev (rel_list 0 (nb_rel env)) in let replace_var_named_declaration id0 id decl = let id' = get_id decl in let id' = if Id.equal id0 id' then id else id' in let vsubst = [id0 , mkVar id] in decl |> set_id id' |> map_constr (replace_vars vsubst) in - let replace_var_named_context id0 id env = - let nc = Environ.named_context env in - let nc' = List.map (replace_var_named_declaration id0 id) nc in - Environ.reset_with_named_context (val_of_named_context nc') env - in let extract_if_neq id = function | Anonymous -> None | Name id' when id_ord id id' = 0 -> None | Name id' -> Some id' in + let open Context.Rel.Declaration in + let (na, c, t) = to_tuple decl in + let open Context.Named.Declaration in + let id = + (* ppedrot: we want to infer nicer names for the refine tactic, but + keeping at the same time backward compatibility in other code + using this function. For now, we only attempt to preserve the + old behaviour of Program, but ultimately, one should do something + about this whole name generation problem. *) + if Flags.is_program_mode () then next_name_away na avoid + else + (** id_of_name_using_hdchar only depends on the rel context which is empty + here *) + next_ident_away (id_of_name_using_hdchar empty_env t na) avoid + in + match extract_if_neq id na with + | Some id0 when not (is_section_variable id0) -> + (* spiwack: if [id<>id0], rather than introducing a new + binding named [id], we will keep [id0] (the name given + by the user) and rename [id0] into [id] in the named + context. Unless [id] is a section variable. *) + let subst = (fst subst, Int.Map.map (replace_vars [id0,mkVar id]) (snd subst)) in + let vsubst = (id0,mkVar id)::vsubst in + let d = match c with + | None -> LocalAssum (id0, subst2 subst vsubst t) + | Some c -> LocalDef (id0, subst2 subst vsubst c, subst2 subst vsubst t) + in + let nc = List.map (replace_var_named_declaration id0 id) nc in + (push_var id0 subst, vsubst, Id.Set.add id avoid, d :: nc) + | _ -> + (* spiwack: if [id0] is a section variable renaming it is + incorrect. We revert to a less robust behaviour where + the new binder has name [id]. Which amounts to the same + behaviour than when [id=id0]. *) + let d = match c with + | None -> LocalAssum (id, subst2 subst vsubst t) + | Some c -> LocalDef (id, subst2 subst vsubst c, subst2 subst vsubst t) + in + (push_var id subst, vsubst, Id.Set.add id avoid, d :: nc) + +let push_rel_context_to_named_context env typ = + (* compute the instances relative to the named context and rel_context *) + let open Context.Named.Declaration in + let ids = List.map get_id (named_context env) in + let avoid = List.fold_right Id.Set.add ids Id.Set.empty in + let inst_vars = List.map mkVar ids in + let inst_rels = List.rev (rel_list 0 (nb_rel env)) in (* move the rel context to a named context and extend the named instance *) (* with vars of the rel context *) (* We do keep the instances corresponding to local definition (see above) *) let (subst, vsubst, _, env) = - Context.Rel.fold_outside - (fun decl (subst, vsubst, avoid, env) -> - let open Context.Rel.Declaration in - let na = get_name decl in - let c = get_value decl in - let t = get_type decl in - let open Context.Named.Declaration in - let id = - (* ppedrot: we want to infer nicer names for the refine tactic, but - keeping at the same time backward compatibility in other code - using this function. For now, we only attempt to preserve the - old behaviour of Program, but ultimately, one should do something - about this whole name generation problem. *) - if Flags.is_program_mode () then next_name_away na avoid - else next_ident_away (id_of_name_using_hdchar env t na) avoid - in - match extract_if_neq id na with - | Some id0 when not (is_section_variable id0) -> - (* spiwack: if [id<>id0], rather than introducing a new - binding named [id], we will keep [id0] (the name given - by the user) and rename [id0] into [id] in the named - context. Unless [id] is a section variable. *) - let subst = List.map (replace_vars [id0,mkVar id]) subst in - let vsubst = (id0,mkVar id)::vsubst in - let d = match c with - | None -> LocalAssum (id0, subst2 subst vsubst t) - | Some c -> LocalDef (id0, subst2 subst vsubst c, subst2 subst vsubst t) - in - let env = replace_var_named_context id0 id env in - (mkVar id0 :: subst, vsubst, id::avoid, push_named d env) - | _ -> - (* spiwack: if [id0] is a section variable renaming it is - incorrect. We revert to a less robust behaviour where - the new binder has name [id]. Which amounts to the same - behaviour than when [id=id0]. *) - let d = match c with - | None -> LocalAssum (id, subst2 subst vsubst t) - | Some c -> LocalDef (id, subst2 subst vsubst c, subst2 subst vsubst t) - in - (mkVar id :: subst, vsubst, id::avoid, push_named d env) - ) - (rel_context env) ~init:([], [], ids, env) in - (named_context_val env, subst2 subst vsubst typ, inst_rels@inst_vars, subst, vsubst) + Context.Rel.fold_outside push_rel_decl_to_named_context + (rel_context env) ~init:(empty_csubst, [], avoid, named_context env) in + (val_of_named_context env, subst2 subst vsubst typ, inst_rels@inst_vars, subst, vsubst) (*------------------------------------* * Entry points to define new evars * diff --git a/engine/evarutil.mli b/engine/evarutil.mli index 111d0f3e8c..c0c81442d5 100644 --- a/engine/evarutil.mli +++ b/engine/evarutil.mli @@ -199,8 +199,20 @@ val clear_hyps_in_evi : env -> evar_map ref -> named_context_val -> types -> val clear_hyps2_in_evi : env -> evar_map ref -> named_context_val -> types -> types -> Id.Set.t -> named_context_val * types * types +type csubst + +val empty_csubst : csubst +val csubst_subst : csubst -> Constr.t -> Constr.t + +type ext_named_context = + csubst * (Id.t * Constr.constr) list * + Id.Set.t * Context.Named.t + +val push_rel_decl_to_named_context : + Context.Rel.Declaration.t -> ext_named_context -> ext_named_context + val push_rel_context_to_named_context : Environ.env -> types -> - named_context_val * types * constr list * constr list * (identifier*constr) list + named_context_val * types * constr list * csubst * (identifier*constr) list val generalize_evar_over_rels : evar_map -> existential -> types * constr list diff --git a/engine/evd.ml b/engine/evd.ml index 196f44760a..6ba8a51120 100644 --- a/engine/evd.ml +++ b/engine/evd.ml @@ -790,16 +790,16 @@ let merge_universe_subst evd subst = let with_context_set ?loc rigid d (a, ctx) = (merge_context_set ?loc rigid d ctx, a) -let new_univ_level_variable ?loc ?name ?(predicative=true) rigid evd = +let new_univ_level_variable ?loc ?name rigid evd = let uctx', u = UState.new_univ_variable ?loc rigid name evd.universes in ({evd with universes = uctx'}, u) -let new_univ_variable ?loc ?name ?(predicative=true) rigid evd = +let new_univ_variable ?loc ?name rigid evd = let uctx', u = UState.new_univ_variable ?loc rigid name evd.universes in ({evd with universes = uctx'}, Univ.Universe.make u) -let new_sort_variable ?loc ?name ?(predicative=true) rigid d = - let (d', u) = new_univ_variable ?loc rigid ?name ~predicative d in +let new_sort_variable ?loc ?name rigid d = + let (d', u) = new_univ_variable ?loc rigid ?name d in (d', Type u) let add_global_univ d u = @@ -1258,6 +1258,12 @@ let pr_instance_status (sc,typ) = | TypeProcessed -> str " [type is checked]" end +let protect f x = + try f x + with e -> str "EXCEPTION: " ++ str (Printexc.to_string e) + +let print_constr a = protect print_constr a + let pr_meta_map mmap = let pr_name = function Name id -> str"[" ++ pr_id id ++ str"]" diff --git a/engine/evd.mli b/engine/evd.mli index d6cf83525c..9424145113 100644 --- a/engine/evd.mli +++ b/engine/evd.mli @@ -508,9 +508,9 @@ val normalize_evar_universe_context_variables : evar_universe_context -> val normalize_evar_universe_context : evar_universe_context -> evar_universe_context -val new_univ_level_variable : ?loc:Loc.t -> ?name:string -> ?predicative:bool -> rigid -> evar_map -> evar_map * Univ.universe_level -val new_univ_variable : ?loc:Loc.t -> ?name:string -> ?predicative:bool -> rigid -> evar_map -> evar_map * Univ.universe -val new_sort_variable : ?loc:Loc.t -> ?name:string -> ?predicative:bool -> rigid -> evar_map -> evar_map * sorts +val new_univ_level_variable : ?loc:Loc.t -> ?name:string -> rigid -> evar_map -> evar_map * Univ.universe_level +val new_univ_variable : ?loc:Loc.t -> ?name:string -> rigid -> evar_map -> evar_map * Univ.universe +val new_sort_variable : ?loc:Loc.t -> ?name:string -> rigid -> evar_map -> evar_map * sorts val add_global_univ : evar_map -> Univ.Level.t -> evar_map diff --git a/engine/namegen.ml b/engine/namegen.ml index 129cb3868e..638adea5d3 100644 --- a/engine/namegen.ml +++ b/engine/namegen.ml @@ -191,18 +191,26 @@ let visible_ids (nenv, c) = let (gseen, vseen, ids) = !accu in let g = global_of_constr c in if not (Refset_env.mem g gseen) then + begin + try let gseen = Refset_env.add g gseen in let short = shortest_qualid_of_global Id.Set.empty g in let dir, id = repr_qualid short in let ids = if DirPath.is_empty dir then Id.Set.add id ids else ids in accu := (gseen, vseen, ids) + with Not_found when !Flags.in_debugger || !Flags.in_toplevel -> () + end | Rel p -> let (gseen, vseen, ids) = !accu in if p > n && not (Int.Set.mem p vseen) then let vseen = Int.Set.add p vseen in let name = try Some (lookup_name_of_rel (p - n) nenv) - with Not_found -> None (* Unbound indice : may happen in debug *) + with Not_found -> + (* Unbound index: may happen in debug and actually also + while computing temporary implicit arguments of an + inductive type *) + None in let ids = match name with | Some (Name id) -> Id.Set.add id ids diff --git a/engine/sigma.ml b/engine/sigma.ml index c7b0bb5a50..9381a33af1 100644 --- a/engine/sigma.ml +++ b/engine/sigma.ml @@ -36,16 +36,16 @@ let new_evar sigma ?naming info = let define evk c sigma = Sigma ((), Evd.define evk c sigma, ()) -let new_univ_level_variable ?loc ?name ?predicative rigid sigma = - let (sigma, u) = Evd.new_univ_level_variable ?loc ?name ?predicative rigid sigma in +let new_univ_level_variable ?loc ?name rigid sigma = + let (sigma, u) = Evd.new_univ_level_variable ?loc ?name rigid sigma in Sigma (u, sigma, ()) -let new_univ_variable ?loc ?name ?predicative rigid sigma = - let (sigma, u) = Evd.new_univ_variable ?loc ?name ?predicative rigid sigma in +let new_univ_variable ?loc ?name rigid sigma = + let (sigma, u) = Evd.new_univ_variable ?loc ?name rigid sigma in Sigma (u, sigma, ()) -let new_sort_variable ?loc ?name ?predicative rigid sigma = - let (sigma, u) = Evd.new_sort_variable ?loc ?name ?predicative rigid sigma in +let new_sort_variable ?loc ?name rigid sigma = + let (sigma, u) = Evd.new_sort_variable ?loc ?name rigid sigma in Sigma (u, sigma, ()) let fresh_sort_in_family ?loc ?rigid env sigma s = diff --git a/engine/sigma.mli b/engine/sigma.mli index aaf603efd8..7473a251b7 100644 --- a/engine/sigma.mli +++ b/engine/sigma.mli @@ -68,11 +68,11 @@ val define : 'r evar -> Constr.t -> 'r t -> (unit, 'r) sigma (** Polymorphic universes *) -val new_univ_level_variable : ?loc:Loc.t -> ?name:string -> ?predicative:bool -> +val new_univ_level_variable : ?loc:Loc.t -> ?name:string -> Evd.rigid -> 'r t -> (Univ.universe_level, 'r) sigma -val new_univ_variable : ?loc:Loc.t -> ?name:string -> ?predicative:bool -> +val new_univ_variable : ?loc:Loc.t -> ?name:string -> Evd.rigid -> 'r t -> (Univ.universe, 'r) sigma -val new_sort_variable : ?loc:Loc.t -> ?name:string -> ?predicative:bool -> +val new_sort_variable : ?loc:Loc.t -> ?name:string -> Evd.rigid -> 'r t -> (Sorts.t, 'r) sigma val fresh_sort_in_family : ?loc:Loc.t -> ?rigid:Evd.rigid -> Environ.env -> diff --git a/ide/coqOps.ml b/ide/coqOps.ml index 18557ab6b4..50b3f2c0a0 100644 --- a/ide/coqOps.ml +++ b/ide/coqOps.ml @@ -339,8 +339,11 @@ object(self) method private show_goals_aux ?(move_insert=false) () = Coq.PrintOpt.set_printing_width proof#width; if move_insert then begin - buffer#place_cursor ~where:self#get_start_of_input; - script#recenter_insert; + let dest = self#get_start_of_input in + if (buffer#get_iter_at_mark `INSERT)#compare dest <= 0 then begin + buffer#place_cursor ~where:dest; + script#recenter_insert + end end; Coq.bind (Coq.goals ~logger:messages#push ()) (function | Fail x -> self#handle_failure_aux ~move_insert x diff --git a/ide/ideutils.ml b/ide/ideutils.ml index f0698a54a3..fe69be9e48 100644 --- a/ide/ideutils.ml +++ b/ide/ideutils.ml @@ -112,6 +112,24 @@ let try_convert s = "(* Fatal error: wrong encoding in input. \ Please choose a correct encoding in the preference panel.*)";; +let export file_name s = + let oc = open_out_bin file_name in + let ending = line_ending#get in + let is_windows = ref false in + for i = 0 to String.length s - 1 do + match s.[i] with + | '\r' -> is_windows := true + | '\n' -> + begin match ending with + | `DEFAULT -> + if !is_windows then (output_char oc '\r'; output_char oc '\n') + else output_char oc '\n' + | `WINDOWS -> output_char oc '\r'; output_char oc '\n' + | `UNIX -> output_char oc '\n' + end + | c -> output_char oc c + done; + close_out oc let try_export file_name s = let s = @@ -134,11 +152,7 @@ let try_export file_name s = Minilib.log ("Error ("^str^") in transcoding: falling back to UTF-8"); s in - try - let oc = open_out file_name in - output_string oc s; - close_out oc; - true + try export file_name s; true with e -> Minilib.log (Printexc.to_string e);false type timer = { run : ms:int -> callback:(unit->bool) -> unit; diff --git a/ide/preferences.ml b/ide/preferences.ml index 3a33bbb1d8..3241a962dc 100644 --- a/ide/preferences.ml +++ b/ide/preferences.ml @@ -121,6 +121,18 @@ let inputenc_of_string s = else if s = "LOCALE" then Elocale else Emanual s) +type line_ending = [ `DEFAULT | `WINDOWS | `UNIX ] + +let line_end_of_string = function +| "unix" -> `UNIX +| "windows" -> `WINDOWS +| _ -> `DEFAULT + +let line_end_to_string = function +| `UNIX -> "unix" +| `WINDOWS -> "windows" +| `DEFAULT -> "default" + let use_default_doc_url = "(automatic)" module Repr = @@ -381,6 +393,10 @@ let stop_before = let reset_on_tab_switch = new preference ~name:["reset_on_tab_switch"] ~init:false ~repr:Repr.(bool) +let line_ending = + let repr = Repr.custom line_end_to_string line_end_of_string in + new preference ~name:["line_ending"] ~init:`DEFAULT ~repr + let vertical_tabs = new preference ~name:["vertical_tabs"] ~init:false ~repr:Repr.(bool) @@ -818,6 +834,15 @@ let configure ?(apply=(fun () -> ())) () = (string_of_inputenc encoding#get) in + let line_ending = + combo + "EOL character" + ~f:(fun s -> line_ending#set (line_end_of_string s)) + ~new_allowed:false + ["unix"; "windows"; "default"] + (line_end_to_string line_ending#get) + in + let source_style = combo "Highlighting style:" ~f:source_style#set ~new_allowed:false @@ -973,7 +998,7 @@ let configure ?(apply=(fun () -> ())) () = Section("Files", Some `DIRECTORY, [global_auto_revert;global_auto_revert_delay; auto_save; auto_save_delay; (* auto_save_name*) - encodings; + encodings; line_ending; ]); Section("Project", Some (`STOCK "gtk-page-setup"), [project_file_name;read_project; diff --git a/ide/preferences.mli b/ide/preferences.mli index 426b0a328e..801869d1dc 100644 --- a/ide/preferences.mli +++ b/ide/preferences.mli @@ -11,6 +11,7 @@ val style_manager : GSourceView2.source_style_scheme_manager type project_behavior = Ignore_args | Append_args | Subst_args type inputenc = Elocale | Eutf8 | Emanual of string +type line_ending = [ `DEFAULT | `WINDOWS | `UNIX ] type tag = { tag_fg_color : string option; @@ -79,6 +80,7 @@ val window_height : int preference val auto_complete : bool preference val stop_before : bool preference val reset_on_tab_switch : bool preference +val line_ending : line_ending preference val vertical_tabs : bool preference val opposite_tabs : bool preference val background_color : string preference diff --git a/interp/constrintern.ml b/interp/constrintern.ml index fb1baae0a8..30016dedcf 100644 --- a/interp/constrintern.ml +++ b/interp/constrintern.ml @@ -432,11 +432,6 @@ let intern_assumption intern lvar env nal bk ty = let env, b = intern_generalized_binder intern_type lvar env (List.hd nal) b b' t ty in env, b -let obj_string x = - if Obj.is_block (Obj.repr x) then - "tag = " ^ string_of_int (Obj.tag (Obj.repr x)) - else "int_val = " ^ string_of_int (Obj.magic x) - let rec free_vars_of_pat il = function | CPatCstr (loc, c, l1, l2) -> @@ -1083,12 +1078,10 @@ let sort_fields ~complete loc fields completer = match fields with | [] -> None | (first_field_ref, first_field_value):: other_fields -> - let env_error_msg = "Environment corruption for records." in - let first_field_glob_ref = - try global_reference_of_reference first_field_ref - with Not_found -> anomaly (Pp.str env_error_msg) in - let record = - try Recordops.find_projection first_field_glob_ref + let (first_field_glob_ref, record) = + try + let gr = global_reference_of_reference first_field_ref in + (gr, Recordops.find_projection gr) with Not_found -> user_err_loc (loc_of_reference first_field_ref, "intern", pr_reference first_field_ref ++ str": Not a projection") @@ -1099,7 +1092,8 @@ let sort_fields ~complete loc fields completer = let base_constructor = let global_record_id = ConstructRef record.Recordops.s_CONST in try Qualid (loc, shortest_qualid_of_global Id.Set.empty global_record_id) - with Not_found -> anomaly (Pp.str env_error_msg) in + with Not_found -> + anomaly (str "Environment corruption for records") in let (end_index, (* one past the last field index *) first_field_index, (* index of the first field of the record *) proj_list) (* list of projections *) diff --git a/interp/dumpglob.ml b/interp/dumpglob.ml index 931fc1ca40..1e14eeb81e 100644 --- a/interp/dumpglob.ml +++ b/interp/dumpglob.ml @@ -127,9 +127,10 @@ let type_of_global_ref gr = | Globnames.ConstructRef _ -> "constr" let remove_sections dir = - if Libnames.is_dirpath_prefix_of dir (Lib.cwd ()) then + let cwd = Lib.cwd_except_section () in + if Libnames.is_dirpath_prefix_of cwd dir then (* Not yet (fully) discharged *) - Libnames.pop_dirpath_n (Lib.sections_depth ()) (Lib.cwd ()) + cwd else (* Theorem/Lemma outside its outer section of definition *) dir diff --git a/interp/notation_ops.ml b/interp/notation_ops.ml index 6478ade61a..f3e0682bd7 100644 --- a/interp/notation_ops.ml +++ b/interp/notation_ops.ml @@ -1165,7 +1165,7 @@ let match_cases_pattern_list match_fun metas sigma rest x y iter termin lassoc = let l,(terms,onlybinders,termlists,binderlists as sigma) = aux sigma [] rest in (terms,onlybinders,(x,if lassoc then l else List.rev l)::termlists, binderlists) -let rec match_cases_pattern metas (terms,x,termlists,y as sigma) a1 a2 = +let rec match_cases_pattern metas (terms,(),termlists,() as sigma) a1 a2 = match (a1,a2) with | r1, NVar id2 when Id.List.mem_assoc id2 metas -> (bind_env_cases_pattern sigma id2 r1),(0,[]) | PatVar (_,Anonymous), NHole _ -> sigma,(0,[]) diff --git a/kernel/context.ml b/kernel/context.ml index 71969be859..43be9fc4f0 100644 --- a/kernel/context.ml +++ b/kernel/context.ml @@ -142,6 +142,11 @@ struct match decl with | LocalAssum (n,ty) -> f ty acc | LocalDef (n,v,ty) -> f ty (f v acc) + + let to_tuple = function + | LocalAssum (na, ty) -> na, None, ty + | LocalDef (na, v, ty) -> na, Some v, ty + end (** Rel-context is represented as a list of declarations. diff --git a/kernel/context.mli b/kernel/context.mli index ecc3987a5a..7c652ac5c2 100644 --- a/kernel/context.mli +++ b/kernel/context.mli @@ -80,6 +80,8 @@ sig (** Reduce all terms in a given declaration to a single value. *) val fold : (Constr.t -> 'a -> 'a) -> t -> 'a -> 'a + + val to_tuple : t -> Name.t * Constr.t option * Constr.t end (** Rel-context is represented as a list of declarations. diff --git a/kernel/vconv.ml b/kernel/vconv.ml index c729a6ce29..894f5296a8 100644 --- a/kernel/vconv.ml +++ b/kernel/vconv.ml @@ -116,14 +116,14 @@ and conv_atom env pb k a1 stk1 a2 stk2 cu = | Atype _ , _ | _, Atype _ -> assert false | Aind _, _ | Aid _, _ -> raise NotConvertible -and conv_stack env ?from:(from=0) k stk1 stk2 cu = +and conv_stack env k stk1 stk2 cu = match stk1, stk2 with | [], [] -> cu | Zapp args1 :: stk1, Zapp args2 :: stk2 -> - conv_stack env k stk1 stk2 (conv_arguments env ~from:from k args1 args2 cu) + conv_stack env k stk1 stk2 (conv_arguments env k args1 args2 cu) | Zfix(f1,args1) :: stk1, Zfix(f2,args2) :: stk2 -> conv_stack env k stk1 stk2 - (conv_arguments env ~from:from k args1 args2 (conv_fix env k f1 f2 cu)) + (conv_arguments env k args1 args2 (conv_fix env k f1 f2 cu)) | Zswitch sw1 :: stk1, Zswitch sw2 :: stk2 -> if check_switch sw1 sw2 then let vt1,vt2 = type_of_switch sw1, type_of_switch sw2 in diff --git a/lib/cList.ml b/lib/cList.ml index 602bba6a5c..c8283e3c71 100644 --- a/lib/cList.ml +++ b/lib/cList.ml @@ -601,19 +601,35 @@ let filter2 f l1 l2 = filter2_loop f c1 c2 l1 l2; (c1.tail, c2.tail) -let rec map_filter f = function - | [] -> [] - | x::l -> - let l' = map_filter f l in - match f x with None -> l' | Some y -> y::l' +let rec map_filter_loop f p = function + | [] -> () + | x :: l -> + match f x with + | None -> map_filter_loop f p l + | Some y -> + let c = { head = y; tail = [] } in + p.tail <- cast c; + map_filter_loop f c l + +let map_filter f l = + let c = { head = Obj.magic 0; tail = [] } in + map_filter_loop f c l; + c.tail -let map_filter_i f = - let rec aux i = function - | [] -> [] - | x::l -> - let l' = aux (succ i) l in - match f i x with None -> l' | Some y -> y::l' - in aux 0 +let rec map_filter_i_loop f i p = function + | [] -> () + | x :: l -> + match f i x with + | None -> map_filter_i_loop f (succ i) p l + | Some y -> + let c = { head = y; tail = [] } in + p.tail <- cast c; + map_filter_i_loop f (succ i) c l + +let map_filter_i f l = + let c = { head = Obj.magic 0; tail = [] } in + map_filter_i_loop f 0 c l; + c.tail let rec filter_with filter l = match filter, l with | [], [] -> [] diff --git a/library/declare.mli b/library/declare.mli index 8dd24d2780..7824506da0 100644 --- a/library/declare.mli +++ b/library/declare.mli @@ -34,14 +34,6 @@ val declare_variable : variable -> variable_declaration -> object_name type constant_declaration = Safe_typing.private_constants constant_entry * logical_kind -(** [declare_constant id cd] declares a global declaration - (constant/parameter) with name [id] in the current section; it returns - the full path of the declaration - - internal specify if the constant has been created by the kernel or by the - user, and in the former case, if its errors should be silent - - *) type internal_flag = | UserAutomaticRequest | InternalTacticRequest @@ -53,6 +45,12 @@ val definition_entry : ?fix_exn:Future.fix_exn -> ?poly:polymorphic -> ?univs:Univ.universe_context -> ?eff:Safe_typing.private_constants -> constr -> Safe_typing.private_constants definition_entry +(** [declare_constant id cd] declares a global declaration + (constant/parameter) with name [id] in the current section; it returns + the full path of the declaration + + internal specify if the constant has been created by the kernel or by the + user, and in the former case, if its errors should be silent *) val declare_constant : ?internal:internal_flag -> ?local:bool -> Id.t -> ?export_seff:bool -> constant_declaration -> constant diff --git a/library/impargs.ml b/library/impargs.ml index 6da7e21100..bce7a15cbe 100644 --- a/library/impargs.ml +++ b/library/impargs.ml @@ -68,10 +68,9 @@ let is_reversible_pattern_implicit_args () = !implicit_args.reversible_pattern let is_contextual_implicit_args () = !implicit_args.contextual let is_maximal_implicit_args () = !implicit_args.maximal -let with_implicits flags f x = +let with_implicit_protection f x = let oflags = !implicit_args in try - implicit_args := flags; let rslt = f x in implicit_args := oflags; rslt diff --git a/library/impargs.mli b/library/impargs.mli index 34e529ca2c..3919a519c9 100644 --- a/library/impargs.mli +++ b/library/impargs.mli @@ -29,8 +29,7 @@ val is_reversible_pattern_implicit_args : unit -> bool val is_contextual_implicit_args : unit -> bool val is_maximal_implicit_args : unit -> bool -type implicits_flags -val with_implicits : implicits_flags -> ('a -> 'b) -> 'a -> 'b +val with_implicit_protection : ('a -> 'b) -> 'a -> 'b (** {6 ... } *) (** An [implicits_list] is a list of positions telling which arguments @@ -136,14 +135,5 @@ val select_impargs_size : int -> implicits_list list -> implicit_status list val select_stronger_impargs : implicits_list list -> implicit_status list -type implicit_interactive_request - -type implicit_discharge_request = - | ImplLocal - | ImplConstant of constant * implicits_flags - | ImplMutualInductive of mutual_inductive * implicits_flags - | ImplInteractive of global_reference * implicits_flags * - implicit_interactive_request - val explicitation_eq : Constrexpr.explicitation -> Constrexpr.explicitation -> bool (** Equality on [explicitation]. *) diff --git a/ltac/ltac.mllib b/ltac/ltac.mllib index 65ed114cff..fc51e48ae4 100644 --- a/ltac/ltac.mllib +++ b/ltac/ltac.mllib @@ -1,3 +1,4 @@ +Taccoerce Tacsubst Tacenv Tactic_debug diff --git a/ltac/profile_ltac.ml b/ltac/profile_ltac.ml index f332e1a0d5..bea02e3dcb 100644 --- a/ltac/profile_ltac.ml +++ b/ltac/profile_ltac.ml @@ -139,7 +139,7 @@ let string_of_call ck = let s = string_of_ppcmds (match ck with - | Tacexpr.LtacNotationCall s -> Names.KerName.print s + | Tacexpr.LtacNotationCall s -> Pptactic.pr_alias_key s | Tacexpr.LtacNameCall cst -> Pptactic.pr_ltac_constant cst | Tacexpr.LtacVarCall (id, t) -> Nameops.pr_id id | Tacexpr.LtacAtomCall te -> diff --git a/ltac/rewrite.ml b/ltac/rewrite.ml index e327deda02..7acad20d20 100644 --- a/ltac/rewrite.ml +++ b/ltac/rewrite.ml @@ -438,14 +438,22 @@ let split_head = function hd :: tl -> hd, tl | [] -> assert(false) +let eq_pb (ty, env, x, y as pb) (ty', env', x', y' as pb') = + pb == pb' || (ty == ty' && Constr.equal x x' && Constr.equal y y') + +let problem_inclusion x y = + List.for_all (fun pb -> List.exists (fun pb' -> eq_pb pb pb') y) x + let evd_convertible env evd x y = try - let evd = Evarconv.the_conv_x env x y evd in (* Unfortunately, the_conv_x might say they are unifiable even if some - unsolvable constraints remain, so we check them here *) - let evd = Evarconv.consider_remaining_unif_problems env evd in - let () = Evarconv.check_problems_are_solved env evd in - Some evd + unsolvable constraints remain, so we check that this unification + does not introduce any new problem. *) + let _, pbs = Evd.extract_all_conv_pbs evd in + let evd' = Evarconv.the_conv_x env x y evd in + let _, pbs' = Evd.extract_all_conv_pbs evd' in + if evd' == evd || problem_inclusion pbs' pbs then Some evd' + else None with e when CErrors.noncritical e -> None let convertible env evd x y = @@ -583,7 +591,7 @@ let general_rewrite_unif_flags () = Unification.modulo_conv_on_closed_terms = Some ts; Unification.use_evars_eagerly_in_conv_on_closed_terms = true; Unification.modulo_delta = ts; - Unification.modulo_delta_types = ts; + Unification.modulo_delta_types = full_transparent_state; Unification.modulo_betaiota = true } in { Unification.core_unify_flags = core_flags; @@ -1432,17 +1440,8 @@ let rewrite_with l2r flags c occs : strategy = { strategy = fun ({ state = () } as input) -> let unify env evars t = let (sigma, cstrs) = evars in - let ans = - try Some (refresh_hypinfo env sigma c) - with e when Class_tactics.catchable e -> None - in - match ans with - | None -> None - | Some (sigma, rew) -> - let rew = unify_eqn rew l2r flags env (sigma, cstrs) None t in - match rew with - | None -> None - | Some rew -> Some rew + let (sigma, rew) = refresh_hypinfo env sigma c in + unify_eqn rew l2r flags env (sigma, cstrs) None t in let app = apply_rule unify occs in let strat = diff --git a/tactics/taccoerce.ml b/ltac/taccoerce.ml index 0110510d35..0110510d35 100644 --- a/tactics/taccoerce.ml +++ b/ltac/taccoerce.ml diff --git a/tactics/taccoerce.mli b/ltac/taccoerce.mli index 0b67f8726e..0b67f8726e 100644 --- a/tactics/taccoerce.mli +++ b/ltac/taccoerce.mli diff --git a/plugins/extraction/modutil.ml b/plugins/extraction/modutil.ml index 864d90a0f2..60fe8e7620 100644 --- a/plugins/extraction/modutil.ml +++ b/plugins/extraction/modutil.ml @@ -310,7 +310,7 @@ let base_r = function let reset_needed, add_needed, add_needed_mp, found_needed, is_needed = let needed = ref Refset'.empty and needed_mps = ref MPset.empty in - ((fun l -> needed := Refset'.empty; needed_mps := MPset.empty), + ((fun () -> needed := Refset'.empty; needed_mps := MPset.empty), (fun r -> needed := Refset'.add (base_r r) !needed), (fun mp -> needed_mps := MPset.add mp !needed_mps), (fun r -> needed := Refset'.remove (base_r r) !needed), diff --git a/plugins/romega/ReflOmegaCore.v b/plugins/romega/ReflOmegaCore.v index 5e43dfc42d..187601fc62 100644 --- a/plugins/romega/ReflOmegaCore.v +++ b/plugins/romega/ReflOmegaCore.v @@ -1451,27 +1451,27 @@ Ltac loop t := | (Tint ?X1) => loop X1 (* Eliminations *) | match ?X1 with - | EqTerm x x0 => _ - | LeqTerm x x0 => _ + | EqTerm _ _ => _ + | LeqTerm _ _ => _ | TrueTerm => _ | FalseTerm => _ - | Tnot x => _ - | GeqTerm x x0 => _ - | GtTerm x x0 => _ - | LtTerm x x0 => _ - | NeqTerm x x0 => _ - | Tor x x0 => _ - | Tand x x0 => _ - | Timp x x0 => _ - | Tprop x => _ + | Tnot _ => _ + | GeqTerm _ _ => _ + | GtTerm _ _ => _ + | LtTerm _ _ => _ + | NeqTerm _ _ => _ + | Tor _ _ => _ + | Tand _ _ => _ + | Timp _ _ => _ + | Tprop _ => _ end => destruct X1; auto; Simplify | match ?X1 with - | Tint x => _ - | (x + x0)%term => _ - | (x * x0)%term => _ - | (x - x0)%term => _ - | (- x)%term => _ - | [x]%term => _ + | Tint _ => _ + | (_ + _)%term => _ + | (_ * _)%term => _ + | (_ - _)%term => _ + | (- _)%term => _ + | [_]%term => _ end => destruct X1; auto; Simplify | (if beq ?X1 ?X2 then _ else _) => let H := fresh "H" in diff --git a/pretyping/cases.ml b/pretyping/cases.ml index 447a4c487c..fe2b0a5a1a 100644 --- a/pretyping/cases.ml +++ b/pretyping/cases.ml @@ -1871,7 +1871,7 @@ let inh_conv_coerce_to_tycon loc env evdref j tycon = (* We put the tycon inside the arity signature, possibly discovering dependencies. *) let prepare_predicate_from_arsign_tycon env sigma loc tomatchs arsign c = - let nar = List.fold_left (fun n sign -> List.length sign + n) 0 arsign in + let nar = List.fold_left (fun n sign -> Context.Rel.nhyps sign + n) 0 arsign in let subst, len = List.fold_right2 (fun (tm, tmtype) sign (subst, len) -> let signlen = List.length sign in diff --git a/pretyping/detyping.ml b/pretyping/detyping.ml index d4066f387b..85125a502e 100644 --- a/pretyping/detyping.ml +++ b/pretyping/detyping.ml @@ -689,7 +689,7 @@ and detype_binder (lax,isgoal as flags) bk avoid env sigma na body ty c = | BLetIn -> let c = detype (lax,false) avoid env sigma (Option.get body) in (* Heuristic: we display the type if in Prop *) - let s = Retyping.get_sort_family_of (snd env) sigma ty in + let s = try Retyping.get_sort_family_of (snd env) sigma ty with _ when !Flags.in_debugger || !Flags.in_toplevel -> InType (* Can fail because of sigma missing in debugger *) in let c = if s != InProp then c else GCast (dl, c, CastConv (detype (lax,false) avoid env sigma ty)) in GLetIn (dl, na', c, r) diff --git a/pretyping/pretyping.ml b/pretyping/pretyping.ml index 187eba16b6..1ef96e0344 100644 --- a/pretyping/pretyping.ml +++ b/pretyping/pretyping.ml @@ -68,6 +68,61 @@ open Inductiveops (************************************************************************) +module ExtraEnv = +struct + +type t = { + env : Environ.env; + extra : Evarutil.ext_named_context Lazy.t; + (** Delay the computation of the evar extended environment *) +} + +let get_extra env = + let open Context.Named.Declaration in + let ids = List.map get_id (named_context env) in + let avoid = List.fold_right Id.Set.add ids Id.Set.empty in + Context.Rel.fold_outside push_rel_decl_to_named_context + (Environ.rel_context env) ~init:(empty_csubst, [], avoid, named_context env) + +let make_env env = { env = env; extra = lazy (get_extra env) } +let rel_context env = rel_context env.env + +let push_rel d env = { + env = push_rel d env.env; + extra = lazy (push_rel_decl_to_named_context d (Lazy.force env.extra)); +} + +let pop_rel_context n env = make_env (pop_rel_context n env.env) + +let push_rel_context ctx env = { + env = push_rel_context ctx env.env; + extra = lazy (List.fold_right push_rel_decl_to_named_context ctx (Lazy.force env.extra)); +} + +let lookup_named id env = lookup_named id env.env + +let e_new_evar env evdref ?src ?naming typ = + let subst2 subst vsubst c = csubst_subst subst (replace_vars vsubst c) in + let open Context.Named.Declaration in + let inst_vars = List.map (fun d -> mkVar (get_id d)) (named_context env.env) in + let inst_rels = List.rev (rel_list 0 (nb_rel env.env)) in + let (subst, vsubst, _, nc) = Lazy.force env.extra in + let typ' = subst2 subst vsubst typ in + let instance = inst_rels @ inst_vars in + let sign = val_of_named_context nc in + let sigma = Sigma.Unsafe.of_evar_map !evdref in + let Sigma (e, sigma, _) = new_evar_instance sign sigma typ' ?src ?naming instance in + evdref := Sigma.to_evar_map sigma; + e + +let push_rec_types (lna,typarray,_) env = + let ctxt = Array.map2_i (fun i na t -> Context.Rel.Declaration.LocalAssum (na, lift i t)) lna typarray in + Array.fold_left (fun e assum -> push_rel assum e) env ctxt + +end + +open ExtraEnv + (* An auxiliary function for searching for fixpoint guard indexes *) exception Found of int array @@ -302,9 +357,9 @@ let evar_type_fixpoint loc env evdref lna lar vdefj = let lt = Array.length vdefj in if Int.equal (Array.length lar) lt then for i = 0 to lt-1 do - if not (e_cumul env evdref (vdefj.(i)).uj_type + if not (e_cumul env.ExtraEnv.env evdref (vdefj.(i)).uj_type (lift lt lar.(i))) then - error_ill_typed_rec_body_loc loc env !evdref + error_ill_typed_rec_body_loc loc env.ExtraEnv.env !evdref i lna vdefj lar done @@ -312,7 +367,7 @@ let evar_type_fixpoint loc env evdref lna lar vdefj = let inh_conv_coerce_to_tycon resolve_tc loc env evdref j = function | None -> j | Some t -> - evd_comb2 (Coercion.inh_conv_coerce_to resolve_tc loc env) evdref j t + evd_comb2 (Coercion.inh_conv_coerce_to resolve_tc loc env.ExtraEnv.env) evdref j t let check_instance loc subst = function | [] -> () @@ -361,7 +416,7 @@ let invert_ltac_bound_name lvar env id0 id = str " which is not bound in current context.") let protected_get_type_of env sigma c = - try Retyping.get_type_of ~lax:true env sigma c + try Retyping.get_type_of ~lax:true env.ExtraEnv.env sigma c with Retyping.RetypeError _ -> errorlabstrm "" (str "Cannot reinterpret " ++ quote (print_constr c) ++ @@ -444,7 +499,7 @@ let pretype_global loc rigid env evd gr us = str " universe instances must be greater or equal to Set."); evd, Some (Univ.Instance.of_array (Array.of_list (List.rev l'))) in - Evd.fresh_global ~loc ~rigid ?names:instance env evd gr + Evd.fresh_global ~loc ~rigid ?names:instance env.ExtraEnv.env evd gr let pretype_ref loc evdref env ref us = match ref with @@ -459,7 +514,7 @@ let pretype_ref loc evdref env ref us = | ref -> let evd, c = pretype_global loc univ_flexible env !evdref ref us in let () = evdref := evd in - let ty = Typing.unsafe_type_of env evd c in + let ty = Typing.unsafe_type_of env.ExtraEnv.env evd c in make_judge c ty let judge_of_Type loc evd s = @@ -477,7 +532,7 @@ let pretype_sort loc evdref = function let new_type_evar env evdref loc = let sigma = Sigma.Unsafe.of_evar_map !evdref in let Sigma ((e, _), sigma, _) = - Evarutil.new_type_evar env sigma + Evarutil.new_type_evar env.ExtraEnv.env sigma univ_flexible_alg ~src:(loc,Evar_kinds.InternalHole) in evdref := Sigma.to_evar_map sigma; @@ -489,7 +544,7 @@ let (f_genarg_interp, genarg_interp_hook) = Hook.make () (* in environment [env], with existential variables [evdref] and *) (* the type constraint tycon *) -let rec pretype k0 resolve_tc (tycon : type_constraint) env evdref (lvar : ltac_var_map) t = +let rec pretype k0 resolve_tc (tycon : type_constraint) (env : ExtraEnv.t) evdref (lvar : ltac_var_map) t = let inh_conv_coerce_to_tycon = inh_conv_coerce_to_tycon resolve_tc in let pretype_type = pretype_type k0 resolve_tc in let pretype = pretype k0 resolve_tc in @@ -515,7 +570,7 @@ let rec pretype k0 resolve_tc (tycon : type_constraint) env evdref (lvar : ltac_ let hyps = evar_filtered_context (Evd.find !evdref evk) in let args = pretype_instance k0 resolve_tc env evdref lvar loc hyps evk inst in let c = mkEvar (evk, args) in - let j = (Retyping.get_judgment_of env !evdref c) in + let j = (Retyping.get_judgment_of env.ExtraEnv.env !evdref c) in inh_conv_coerce_to_tycon loc env evdref j tycon | GPatVar (loc,(someta,n)) -> @@ -544,7 +599,7 @@ let rec pretype k0 resolve_tc (tycon : type_constraint) env evdref (lvar : ltac_ | None -> new_type_evar env evdref loc in let ist = lvar.ltac_genargs in - let (c, sigma) = Hook.get f_genarg_interp ty env !evdref ist arg in + let (c, sigma) = Hook.get f_genarg_interp ty env.ExtraEnv.env !evdref ist arg in let () = evdref := sigma in { uj_val = c; uj_type = ty } @@ -578,7 +633,7 @@ let rec pretype k0 resolve_tc (tycon : type_constraint) env evdref (lvar : ltac_ let fixi = match fixkind with | GFix (vn,i) -> i | GCoFix i -> i - in e_conv env evdref ftys.(fixi) t + in e_conv env.ExtraEnv.env evdref ftys.(fixi) t | None -> true in (* Note: bodies are not used by push_rec_types, so [||] is safe *) @@ -617,12 +672,12 @@ let rec pretype k0 resolve_tc (tycon : type_constraint) env evdref (lvar : ltac_ let fixdecls = (names,ftys,fdefs) in let indexes = search_guard - loc env possible_indexes fixdecls + loc env.ExtraEnv.env possible_indexes fixdecls in make_judge (mkFix ((indexes,i),fixdecls)) ftys.(i) | GCoFix i -> let cofix = (i,(names,ftys,fdefs)) in - (try check_cofix env cofix + (try check_cofix env.ExtraEnv.env cofix with reraise -> let (e, info) = CErrors.push reraise in let info = Loc.add_loc info loc in @@ -652,7 +707,7 @@ let rec pretype k0 resolve_tc (tycon : type_constraint) env evdref (lvar : ltac_ if Int.equal npars 0 then [] else try - let IndType (indf, args) = find_rectype env !evdref ty in + let IndType (indf, args) = find_rectype env.ExtraEnv.env !evdref ty in let ((ind',u'),pars) = dest_ind_family indf in if eq_ind ind ind' then pars else (* Let the usual code throw an error *) [] @@ -661,9 +716,9 @@ let rec pretype k0 resolve_tc (tycon : type_constraint) env evdref (lvar : ltac_ in let app_f = match kind_of_term fj.uj_val with - | Const (p, u) when Environ.is_projection p env -> + | Const (p, u) when Environ.is_projection p env.ExtraEnv.env -> let p = Projection.make p false in - let pb = Environ.lookup_projection p env in + let pb = Environ.lookup_projection p env.ExtraEnv.env in let npars = pb.Declarations.proj_npars in fun n -> if n == npars + 1 then fun _ v -> mkProj (p, v) @@ -674,8 +729,8 @@ let rec pretype k0 resolve_tc (tycon : type_constraint) env evdref (lvar : ltac_ | [] -> resj | c::rest -> let argloc = loc_of_glob_constr c in - let resj = evd_comb1 (Coercion.inh_app_fun resolve_tc env) evdref resj in - let resty = whd_all env !evdref resj.uj_type in + let resj = evd_comb1 (Coercion.inh_app_fun resolve_tc env.ExtraEnv.env) evdref resj in + let resty = whd_all env.ExtraEnv.env !evdref resj.uj_type in match kind_of_term resty with | Prod (na,c1,c2) -> let tycon = Some c1 in @@ -684,7 +739,7 @@ let rec pretype k0 resolve_tc (tycon : type_constraint) env evdref (lvar : ltac_ match candargs with | [] -> [], j_val hj | arg :: args -> - if e_conv env evdref (j_val hj) arg then + if e_conv env.ExtraEnv.env evdref (j_val hj) arg then args, nf_evar !evdref (j_val hj) else [], j_val hj in @@ -695,7 +750,7 @@ let rec pretype k0 resolve_tc (tycon : type_constraint) env evdref (lvar : ltac_ | _ -> let hj = pretype empty_tycon env evdref lvar c in error_cant_apply_not_functional_loc - (Loc.merge floc argloc) env !evdref + (Loc.merge floc argloc) env.ExtraEnv.env !evdref resj [hj] in let resj = apply_rec env 1 fj candargs args in @@ -703,13 +758,13 @@ let rec pretype k0 resolve_tc (tycon : type_constraint) env evdref (lvar : ltac_ match evar_kind_of_term !evdref resj.uj_val with | App (f,args) -> let f = whd_evar !evdref f in - if is_template_polymorphic env f then + if is_template_polymorphic env.ExtraEnv.env f then (* Special case for inductive type applications that must be refreshed right away. *) let sigma = !evdref in let c = mkApp (f,Array.map (whd_evar sigma) args) in - let c = evd_comb1 (Evarsolve.refresh_universes (Some true) env) evdref c in - let t = Retyping.get_type_of env !evdref c in + let c = evd_comb1 (Evarsolve.refresh_universes (Some true) env.ExtraEnv.env) evdref c in + let t = Retyping.get_type_of env.ExtraEnv.env !evdref c in make_judge c (* use this for keeping evars: resj.uj_val *) t else resj | _ -> resj @@ -722,11 +777,11 @@ let rec pretype k0 resolve_tc (tycon : type_constraint) env evdref (lvar : ltac_ match tycon with | None -> evd, tycon | Some ty -> - let evd, ty' = Coercion.inh_coerce_to_prod loc env evd ty in + let evd, ty' = Coercion.inh_coerce_to_prod loc env.ExtraEnv.env evd ty in evd, Some ty') evdref tycon in - let (name',dom,rng) = evd_comb1 (split_tycon loc env) evdref tycon' in + let (name',dom,rng) = evd_comb1 (split_tycon loc env.ExtraEnv.env) evdref tycon' in let dom_valcon = valcon_of_tycon dom in let j = pretype_type dom_valcon env evdref lvar c1 in (* The name specified by ltac is used also to create bindings. So @@ -735,7 +790,7 @@ let rec pretype k0 resolve_tc (tycon : type_constraint) env evdref (lvar : ltac_ let var = LocalAssum (name, j.utj_val) in let j' = pretype rng (push_rel var env) evdref lvar c2 in let name = ltac_interp_name lvar name in - let resj = judge_of_abstraction env (orelse_name name name') j j' in + let resj = judge_of_abstraction env.ExtraEnv.env (orelse_name name name') j j' in inh_conv_coerce_to_tycon loc env evdref resj tycon | GProd(loc,name,bk,c1,c2) -> @@ -749,13 +804,13 @@ let rec pretype k0 resolve_tc (tycon : type_constraint) env evdref (lvar : ltac_ { j with utj_val = lift 1 j.utj_val } | Name _ -> let var = (name,j.utj_val) in - let env' = push_rel_assum var env in + let env' = ExtraEnv.make_env (push_rel_assum var env.ExtraEnv.env) in pretype_type empty_valcon env' evdref lvar c2 in let name = ltac_interp_name lvar name in let resj = try - judge_of_product env name j j' + judge_of_product env.ExtraEnv.env name j j' with TypeError _ as e -> let (e, info) = CErrors.push e in let info = Loc.add_loc info loc in @@ -771,7 +826,7 @@ let rec pretype k0 resolve_tc (tycon : type_constraint) env evdref (lvar : ltac_ | _ -> pretype empty_tycon env evdref lvar c1 in let t = evd_comb1 (Evarsolve.refresh_universes - ~onlyalg:true ~status:Evd.univ_flexible (Some false) env) + ~onlyalg:true ~status:Evd.univ_flexible (Some false) env.ExtraEnv.env) evdref j.uj_type in (* The name specified by ltac is used also to create bindings. So the substitution must also be applied on variables before they are @@ -786,12 +841,12 @@ let rec pretype k0 resolve_tc (tycon : type_constraint) env evdref (lvar : ltac_ | GLetTuple (loc,nal,(na,po),c,d) -> let cj = pretype empty_tycon env evdref lvar c in let (IndType (indf,realargs)) = - try find_rectype env !evdref cj.uj_type + try find_rectype env.ExtraEnv.env !evdref cj.uj_type with Not_found -> let cloc = loc_of_glob_constr c in - error_case_not_inductive_loc cloc env !evdref cj + error_case_not_inductive_loc cloc env.ExtraEnv.env !evdref cj in - let cstrs = get_constructors env indf in + let cstrs = get_constructors env.ExtraEnv.env indf in if not (Int.equal (Array.length cstrs) 1) then user_err_loc (loc,"",str "Destructing let is only for inductive types" ++ str " with one constructor."); @@ -800,7 +855,7 @@ let rec pretype k0 resolve_tc (tycon : type_constraint) env evdref (lvar : ltac_ user_err_loc (loc,"", str "Destructing let on this type expects " ++ int cs.cs_nargs ++ str " variables."); let fsign, record = - match get_projections env indf with + match get_projections env.ExtraEnv.env indf with | None -> List.map2 set_name (List.rev nal) cs.cs_args, false | Some ps -> @@ -821,36 +876,36 @@ let rec pretype k0 resolve_tc (tycon : type_constraint) env evdref (lvar : ltac_ let nal = List.rev nal in let fsign = List.map2 set_name nal fsign in let f = it_mkLambda_or_LetIn f fsign in - let ci = make_case_info env (fst ind) LetStyle in + let ci = make_case_info env.ExtraEnv.env (fst ind) LetStyle in mkCase (ci, p, cj.uj_val,[|f|]) else it_mkLambda_or_LetIn f fsign in let env_f = push_rel_context fsign env in (* Make dependencies from arity signature impossible *) let arsgn = - let arsgn,_ = get_arity env indf in + let arsgn,_ = get_arity env.ExtraEnv.env indf in if not !allow_anonymous_refs then List.map (set_name Anonymous) arsgn else arsgn in - let psign = LocalAssum (na, build_dependent_inductive env indf) :: arsgn in + let psign = LocalAssum (na, build_dependent_inductive env.ExtraEnv.env indf) :: arsgn in let nar = List.length arsgn in (match po with | Some p -> let env_p = push_rel_context psign env in let pj = pretype_type empty_valcon env_p evdref lvar p in let ccl = nf_evar !evdref pj.utj_val in - let psign = make_arity_signature env true indf in (* with names *) + let psign = make_arity_signature env.ExtraEnv.env true indf in (* with names *) let p = it_mkLambda_or_LetIn ccl psign in let inst = (Array.to_list cs.cs_concl_realargs) @[build_dependent_constructor cs] in let lp = lift cs.cs_nargs p in - let fty = hnf_lam_applist env !evdref lp inst in + let fty = hnf_lam_applist env.ExtraEnv.env !evdref lp inst in let fj = pretype (mk_tycon fty) env_f evdref lvar d in let v = let ind,_ = dest_ind_family indf in - Typing.check_allowed_sort env !evdref ind cj.uj_val p; + Typing.check_allowed_sort env.ExtraEnv.env !evdref ind cj.uj_val p; obj ind p cj.uj_val fj.uj_val in { uj_val = v; uj_type = substl (realargs@[cj.uj_val]) ccl } @@ -863,37 +918,37 @@ let rec pretype k0 resolve_tc (tycon : type_constraint) env evdref (lvar : ltac_ if noccur_between 1 cs.cs_nargs ccl then lift (- cs.cs_nargs) ccl else - error_cant_find_case_type_loc loc env !evdref + error_cant_find_case_type_loc loc env.ExtraEnv.env !evdref cj.uj_val in (* let ccl = refresh_universes ccl in *) let p = it_mkLambda_or_LetIn (lift (nar+1) ccl) psign in let v = let ind,_ = dest_ind_family indf in - Typing.check_allowed_sort env !evdref ind cj.uj_val p; + Typing.check_allowed_sort env.ExtraEnv.env !evdref ind cj.uj_val p; obj ind p cj.uj_val fj.uj_val in { uj_val = v; uj_type = ccl }) | GIf (loc,c,(na,po),b1,b2) -> let cj = pretype empty_tycon env evdref lvar c in let (IndType (indf,realargs)) = - try find_rectype env !evdref cj.uj_type + try find_rectype env.ExtraEnv.env !evdref cj.uj_type with Not_found -> let cloc = loc_of_glob_constr c in - error_case_not_inductive_loc cloc env !evdref cj in - let cstrs = get_constructors env indf in + error_case_not_inductive_loc cloc env.ExtraEnv.env !evdref cj in + let cstrs = get_constructors env.ExtraEnv.env indf in if not (Int.equal (Array.length cstrs) 2) then user_err_loc (loc,"", str "If is only for inductive types with two constructors."); let arsgn = - let arsgn,_ = get_arity env indf in + let arsgn,_ = get_arity env.ExtraEnv.env indf in if not !allow_anonymous_refs then (* Make dependencies from arity signature impossible *) List.map (set_name Anonymous) arsgn else arsgn in let nar = List.length arsgn in - let psign = LocalAssum (na, build_dependent_inductive env indf) :: arsgn in + let psign = LocalAssum (na, build_dependent_inductive env.ExtraEnv.env indf) :: arsgn in let pred,p = match po with | Some p -> let env_p = push_rel_context psign env in @@ -931,9 +986,9 @@ let rec pretype k0 resolve_tc (tycon : type_constraint) env evdref (lvar : ltac_ let b2 = f cstrs.(1) b2 in let v = let ind,_ = dest_ind_family indf in - let ci = make_case_info env (fst ind) IfStyle in + let ci = make_case_info env.ExtraEnv.env (fst ind) IfStyle in let pred = nf_evar !evdref pred in - Typing.check_allowed_sort env !evdref ind cj.uj_val pred; + Typing.check_allowed_sort env.ExtraEnv.env !evdref ind cj.uj_val pred; mkCase (ci, pred, cj.uj_val, [|b1;b2|]) in let cj = { uj_val = v; uj_type = p } in @@ -941,20 +996,20 @@ let rec pretype k0 resolve_tc (tycon : type_constraint) env evdref (lvar : ltac_ | GCases (loc,sty,po,tml,eqns) -> Cases.compile_cases loc sty - ((fun vtyc env evdref -> pretype vtyc env evdref lvar),evdref) - tycon env (* loc *) (po,tml,eqns) + ((fun vtyc env evdref -> pretype vtyc (make_env env) evdref lvar),evdref) + tycon env.ExtraEnv.env (* loc *) (po,tml,eqns) | GCast (loc,c,k) -> let cj = match k with | CastCoerce -> let cj = pretype empty_tycon env evdref lvar c in - evd_comb1 (Coercion.inh_coerce_to_base loc env) evdref cj + evd_comb1 (Coercion.inh_coerce_to_base loc env.ExtraEnv.env) evdref cj | CastConv t | CastVM t | CastNative t -> let k = (match k with CastVM _ -> VMcast | CastNative _ -> NATIVEcast | _ -> DEFAULTcast) in let tj = pretype_type empty_valcon env evdref lvar t in let tval = evd_comb1 (Evarsolve.refresh_universes - ~onlyalg:true ~status:Evd.univ_flexible (Some false) env) + ~onlyalg:true ~status:Evd.univ_flexible (Some false) env.ExtraEnv.env) evdref tj.utj_val in let tval = nf_evar !evdref tval in let cj, tval = match k with @@ -962,22 +1017,22 @@ let rec pretype k0 resolve_tc (tycon : type_constraint) env evdref (lvar : ltac_ let cj = pretype empty_tycon env evdref lvar c in let cty = nf_evar !evdref cj.uj_type and tval = nf_evar !evdref tval in if not (occur_existential cty || occur_existential tval) then - let (evd,b) = Reductionops.vm_infer_conv env !evdref cty tval in + let (evd,b) = Reductionops.vm_infer_conv env.ExtraEnv.env !evdref cty tval in if b then (evdref := evd; cj, tval) else - error_actual_type_loc loc env !evdref cj tval - (ConversionFailed (env,cty,tval)) + error_actual_type_loc loc env.ExtraEnv.env !evdref cj tval + (ConversionFailed (env.ExtraEnv.env,cty,tval)) else user_err_loc (loc,"",str "Cannot check cast with vm: " ++ str "unresolved arguments remain.") | NATIVEcast -> let cj = pretype empty_tycon env evdref lvar c in let cty = nf_evar !evdref cj.uj_type and tval = nf_evar !evdref tval in begin - let (evd,b) = Nativenorm.native_infer_conv env !evdref cty tval in + let (evd,b) = Nativenorm.native_infer_conv env.ExtraEnv.env !evdref cty tval in if b then (evdref := evd; cj, tval) else - error_actual_type_loc loc env !evdref cj tval - (ConversionFailed (env,cty,tval)) + error_actual_type_loc loc env.ExtraEnv.env !evdref cj tval + (ConversionFailed (env.ExtraEnv.env,cty,tval)) end | _ -> pretype (mk_tycon tval) env evdref lvar c, tval @@ -998,11 +1053,11 @@ and pretype_instance k0 resolve_tc env evdref lvar loc hyps evk update = with Not_found -> try let (n,_,t') = lookup_rel_id id (rel_context env) in - if is_conv env !evdref t t' then mkRel n, update else raise Not_found + if is_conv env.ExtraEnv.env !evdref t t' then mkRel n, update else raise Not_found with Not_found -> try let t' = lookup_named id env |> get_type in - if is_conv env !evdref t t' then mkVar id, update else raise Not_found + if is_conv env.ExtraEnv.env !evdref t t' then mkVar id, update else raise Not_found with Not_found -> user_err_loc (loc,"",str "Cannot interpret " ++ pr_existential_key !evdref evk ++ @@ -1013,17 +1068,17 @@ and pretype_instance k0 resolve_tc env evdref lvar loc hyps evk update = Array.map_of_list snd subst (* [pretype_type valcon env evdref lvar c] coerces [c] into a type *) -and pretype_type k0 resolve_tc valcon env evdref lvar = function +and pretype_type k0 resolve_tc valcon (env : ExtraEnv.t) evdref lvar = function | GHole (loc, knd, naming, None) -> (match valcon with | Some v -> let s = let sigma = !evdref in - let t = Retyping.get_type_of env sigma v in - match kind_of_term (whd_all env sigma t) with + let t = Retyping.get_type_of env.ExtraEnv.env sigma v in + match kind_of_term (whd_all env.ExtraEnv.env sigma t) with | Sort s -> s | Evar ev when is_Type (existential_type sigma ev) -> - evd_comb1 (define_evar_as_sort env) evdref ev + evd_comb1 (define_evar_as_sort env.ExtraEnv.env) evdref ev | _ -> anomaly (Pp.str "Found a type constraint which is not a type") in { utj_val = v; @@ -1036,16 +1091,17 @@ and pretype_type k0 resolve_tc valcon env evdref lvar = function | c -> let j = pretype k0 resolve_tc empty_tycon env evdref lvar c in let loc = loc_of_glob_constr c in - let tj = evd_comb1 (Coercion.inh_coerce_to_sort loc env) evdref j in + let tj = evd_comb1 (Coercion.inh_coerce_to_sort loc env.ExtraEnv.env) evdref j in match valcon with | None -> tj | Some v -> - if e_cumul env evdref v tj.utj_val then tj + if e_cumul env.ExtraEnv.env evdref v tj.utj_val then tj else error_unexpected_type_loc - (loc_of_glob_constr c) env !evdref tj.utj_val v + (loc_of_glob_constr c) env.ExtraEnv.env !evdref tj.utj_val v let ise_pretype_gen flags env sigma lvar kind c = + let env = make_env env in let evdref = ref sigma in let k0 = Context.Rel.length (rel_context env) in let c' = match kind with @@ -1056,7 +1112,7 @@ let ise_pretype_gen flags env sigma lvar kind c = | IsType -> (pretype_type k0 flags.use_typeclasses empty_valcon env evdref lvar c).utj_val in - process_inference_flags flags env sigma (!evdref,c') + process_inference_flags flags env.ExtraEnv.env sigma (!evdref,c') let default_inference_flags fail = { use_typeclasses = true; @@ -1088,19 +1144,21 @@ let on_judgment f j = {uj_val = c; uj_type = t} let understand_judgment env sigma c = + let env = make_env env in let evdref = ref sigma in let k0 = Context.Rel.length (rel_context env) in let j = pretype k0 true empty_tycon env evdref empty_lvar c in let j = on_judgment (fun c -> - let evd, c = process_inference_flags all_and_fail_flags env sigma (!evdref,c) in + let evd, c = process_inference_flags all_and_fail_flags env.ExtraEnv.env sigma (!evdref,c) in evdref := evd; c) j in j, Evd.evar_universe_context !evdref let understand_judgment_tcc env evdref c = + let env = make_env env in let k0 = Context.Rel.length (rel_context env) in let j = pretype k0 true empty_tycon env evdref empty_lvar c in on_judgment (fun c -> - let (evd,c) = process_inference_flags all_no_fail_flags env Evd.empty (!evdref,c) in + let (evd,c) = process_inference_flags all_no_fail_flags env.ExtraEnv.env Evd.empty (!evdref,c) in evdref := evd; c) j let ise_pretype_gen_ctx flags env sigma lvar kind c = @@ -1149,3 +1207,9 @@ let type_uconstr ?(flags = constr_flags) let (sigma, c) = understand_ltac flags env sigma vars expected_type term in Sigma.Unsafe.of_pair (c, sigma) end } + +let pretype k0 resolve_tc typcon env evdref lvar t = + pretype k0 resolve_tc typcon (make_env env) evdref lvar t + +let pretype_type k0 resolve_tc valcon env evdref lvar t = + pretype_type k0 resolve_tc valcon (make_env env) evdref lvar t diff --git a/pretyping/typing.ml b/pretyping/typing.ml index 0e4885bead..696d419afe 100644 --- a/pretyping/typing.ml +++ b/pretyping/typing.ml @@ -110,18 +110,18 @@ let e_type_case_branches env evdref (ind,largs) pj c = let nparams = inductive_params specif in let (params,realargs) = List.chop nparams largs in let p = pj.uj_val in - let univ = e_is_correct_arity env evdref c pj ind specif params in + let () = e_is_correct_arity env evdref c pj ind specif params in let lc = build_branches_type ind specif params p in let n = (snd specif).Declarations.mind_nrealdecls in let ty = whd_betaiota !evdref (lambda_applist_assum (n+1) p (realargs@[c])) in - (lc, ty, univ) + (lc, ty) let e_judge_of_case env evdref ci pj cj lfj = let indspec = try find_mrectype env !evdref cj.uj_type with Not_found -> error_case_not_inductive env cj in let _ = check_case_info env (fst indspec) ci in - let (bty,rslty,univ) = e_type_case_branches env evdref indspec pj cj.uj_val in + let (bty,rslty) = e_type_case_branches env evdref indspec pj cj.uj_val in e_check_branch_types env evdref (fst indspec) cj (lfj,bty); { uj_val = mkCase (ci, pj.uj_val, cj.uj_val, Array.map j_val lfj); uj_type = rslty } diff --git a/tactics/elimschemes.ml b/tactics/elimschemes.ml index 99c2d82106..93073fdc7e 100644 --- a/tactics/elimschemes.ml +++ b/tactics/elimschemes.ml @@ -52,19 +52,21 @@ let optimize_non_type_induction_scheme kind dep sort _ ind = let u = Univ.UContext.instance ctx in let ctxset = Univ.ContextSet.of_context ctx in let ectx = Evd.evar_universe_context_of ctxset in - let sigma, c = build_induction_scheme env (Evd.from_ctx ectx) (ind,u) dep sort in + let sigma = Evd.merge_universe_context sigma ectx in + let sigma, c = build_induction_scheme env sigma (ind,u) dep sort in (c, Evd.evar_universe_context sigma), Safe_typing.empty_private_constants let build_induction_scheme_in_type dep sort ind = let env = Global.env () in + let sigma = Evd.from_env env in let ctx = let mib,mip = Inductive.lookup_mind_specif env ind in Declareops.inductive_context mib in let u = Univ.UContext.instance ctx in let ctxset = Univ.ContextSet.of_context ctx in - let ectx = Evd.evar_universe_context_of ctxset in - let sigma, c = build_induction_scheme env (Evd.from_ctx ectx) (ind,u) dep sort in + let sigma = Evd.merge_universe_context sigma (Evd.evar_universe_context_of ctxset) in + let sigma, c = build_induction_scheme env sigma (ind,u) dep sort in c, Evd.evar_universe_context sigma let rect_scheme_kind_from_type = diff --git a/tactics/equality.ml b/tactics/equality.ml index 4aa7ffa7bd..3e5b7b65ff 100644 --- a/tactics/equality.ml +++ b/tactics/equality.ml @@ -629,7 +629,7 @@ let replace_using_leibniz clause c1 c2 l2r unsafe try_prove_eq_opt = in match evd with | None -> - tclFAIL 0 (str"Terms do not have convertible types.") + tclFAIL 0 (str"Terms do not have convertible types") | Some evd -> let e = build_coq_eq () in let sym = build_coq_eq_sym () in @@ -1691,7 +1691,7 @@ let subst_one dep_proof_ok x (hyp,rhs,dir) = && List.exists (fun y -> occur_var_in_decl env y dcl) deps then let id_dest = if !regular_subst_tactic then dest else MoveLast in - (dest,(if is_local_assum dcl then deps else id::deps), (id_dest,id)::allhyps) + (dest,id::deps,(id_dest,id)::allhyps) else (MoveBefore id,deps,allhyps)) hyps diff --git a/tactics/tactics.ml b/tactics/tactics.ml index 38af9a0caa..acc0fa1ca7 100644 --- a/tactics/tactics.ml +++ b/tactics/tactics.ml @@ -1270,7 +1270,7 @@ let clenv_refine_in ?(sidecond_first=false) with_evars ?(with_classes=true) let naming = NamingMustBe (dloc,targetid) in let with_clear = do_replace (Some id) naming in Tacticals.New.tclTHEN - (Proofview.Unsafe.tclEVARS clenv.evd) + (Proofview.Unsafe.tclEVARS (clear_metas clenv.evd)) (if sidecond_first then Tacticals.New.tclTHENFIRST (assert_before_then_gen with_clear naming new_hyp_typ tac) exact_tac @@ -4865,8 +4865,13 @@ let abstract_subproof id gk tac = in let cd = Entries.DefinitionEntry const in let decl = (cd, IsProof Lemma) in - (** ppedrot: seems legit to have abstracted subproofs as local*) - let cst = Declare.declare_constant ~internal:Declare.InternalTacticRequest ~local:true id decl in + let cst () = + (** do not compute the implicit arguments, it may be costly *) + let () = Impargs.make_implicit_args false in + (** ppedrot: seems legit to have abstracted subproofs as local*) + Declare.declare_constant ~internal:Declare.InternalTacticRequest ~local:true id decl + in + let cst = Impargs.with_implicit_protection cst () in (* let evd, lem = Evd.fresh_global (Global.env ()) evd (ConstRef cst) in *) let lem, ctx = Universes.unsafe_constr_of_global (ConstRef cst) in let evd = Evd.set_universe_context evd ectx in diff --git a/tactics/tactics.mllib b/tactics/tactics.mllib index 48722f655a..093302608e 100644 --- a/tactics/tactics.mllib +++ b/tactics/tactics.mllib @@ -12,7 +12,6 @@ Equality Contradiction Inv Leminv -Taccoerce Hints Auto Eauto diff --git a/test-suite/bugs/closed/3070.v b/test-suite/bugs/closed/3070.v new file mode 100644 index 0000000000..7a8feca587 --- /dev/null +++ b/test-suite/bugs/closed/3070.v @@ -0,0 +1,6 @@ +(* Testing subst wrt chains of dependencies *) + +Lemma foo (a1 a2 : Set) (b1 : a1 -> Prop) + (Ha : a1 = a2) (c : a1) (d : b1 c) : True. +Proof. + subst. diff --git a/test-suite/bugs/closed/3886.v b/test-suite/bugs/closed/3886.v new file mode 100644 index 0000000000..2ac4abe54f --- /dev/null +++ b/test-suite/bugs/closed/3886.v @@ -0,0 +1,23 @@ +Require Import Program. + +Inductive Even : nat -> Prop := +| evenO : Even O +| evenS : forall n, Odd n -> Even (S n) +with Odd : nat -> Prop := +| oddS : forall n, Even n -> Odd (S n). + +Program Fixpoint doubleE {n} (e : Even n) : Even (2 * n) + := _ +with doubleO {n} (o : Odd n) : Odd (S (2 * n)) + := _. +Obligations. +Axiom cheat : forall {A}, A. +Obligation 1 of doubleE. +apply cheat. +Qed. + +Obligation 1 of doubleO. +apply cheat. +Qed. + +Check doubleE.
\ No newline at end of file diff --git a/test-suite/bugs/closed/4187.v b/test-suite/bugs/closed/4187.v new file mode 100644 index 0000000000..b13ca36a37 --- /dev/null +++ b/test-suite/bugs/closed/4187.v @@ -0,0 +1,709 @@ +(* Lifted from https://coq.inria.fr/bugs/show_bug.cgi?id=4187 *) +(* File reduced by coq-bug-finder from original input, then from 715 lines to 696 lines *) +(* coqc version 8.4pl5 (December 2014) compiled on Dec 28 2014 03:23:16 with OCaml 4.01.0 + coqtop version 8.4pl5 (December 2014) *) +Set Asymmetric Patterns. +Axiom proof_admitted : False. +Tactic Notation "admit" := case proof_admitted. +Require Import Coq.Lists.List. +Require Import Coq.Setoids.Setoid. +Require Import Coq.Numbers.Natural.Peano.NPeano. +Global Set Implicit Arguments. +Global Generalizable All Variables. +Coercion is_true : bool >-> Sortclass. +Coercion bool_of_sumbool {A B} (x : {A} + {B}) : bool := if x then true else false. +Fixpoint ForallT {T} (P : T -> Type) (ls : list T) : Type + := match ls return Type with + | nil => True + | x::xs => (P x * ForallT P xs)%type + end. +Fixpoint Forall_tails {T} (P : list T -> Type) (ls : list T) : Type + := match ls with + | nil => P nil + | x::xs => (P (x::xs) * Forall_tails P xs)%type + end. + +Module Export ADTSynthesis_DOT_Common_DOT_Wf. +Module Export ADTSynthesis. +Module Export Common. +Module Export Wf. + +Section wf. + Section wf_prod. + Context A B (RA : relation A) (RB : relation B). +Definition prod_relation : relation (A * B). +exact (fun ab a'b' => + RA (fst ab) (fst a'b') \/ (fst a'b' = fst ab /\ RB (snd ab) (snd a'b'))). +Defined. + + Fixpoint well_founded_prod_relation_helper + a b + (wf_A : Acc RA a) (wf_B : well_founded RB) {struct wf_A} + : Acc prod_relation (a, b) + := match wf_A with + | Acc_intro fa => (fix wf_B_rec b' (wf_B' : Acc RB b') : Acc prod_relation (a, b') + := Acc_intro + _ + (fun ab => + match ab as ab return prod_relation ab (a, b') -> Acc prod_relation ab with + | (a'', b'') => + fun pf => + match pf with + | or_introl pf' + => @well_founded_prod_relation_helper + _ _ + (fa _ pf') + wf_B + | or_intror (conj pfa pfb) + => match wf_B' with + | Acc_intro fb + => eq_rect + _ + (fun a'' => Acc prod_relation (a'', b'')) + (wf_B_rec _ (fb _ pfb)) + _ + pfa + end + end + end) + ) b (wf_B b) + end. + + Definition well_founded_prod_relation : well_founded RA -> well_founded RB -> well_founded prod_relation. + Proof. + intros wf_A wf_B [a b]; hnf in *. + apply well_founded_prod_relation_helper; auto. + Defined. + End wf_prod. + + Section wf_projT1. + Context A (B : A -> Type) (R : relation A). +Definition projT1_relation : relation (sigT B). +exact (fun ab a'b' => + R (projT1 ab) (projT1 a'b')). +Defined. + + Definition well_founded_projT1_relation : well_founded R -> well_founded projT1_relation. + Proof. + intros wf [a b]; hnf in *. + induction (wf a) as [a H IH]. + constructor. + intros y r. + specialize (IH _ r (projT2 y)). + destruct y. + exact IH. + Defined. + End wf_projT1. +End wf. + +Section Fix3. + Context A (B : A -> Type) (C : forall a, B a -> Type) (D : forall a b, C a b -> Type) + (R : A -> A -> Prop) (Rwf : well_founded R) + (P : forall a b c, D a b c -> Type) + (F : forall x : A, (forall y : A, R y x -> forall b c d, P y b c d) -> forall b c d, P x b c d). +Definition Fix3 a b c d : @P a b c d. +exact (@Fix { a : A & { b : B a & { c : C b & D c } } } + (fun x y => R (projT1 x) (projT1 y)) + (well_founded_projT1_relation Rwf) + (fun abcd => P (projT2 (projT2 (projT2 abcd)))) + (fun x f => @F (projT1 x) (fun y r b c d => f (existT _ y (existT _ b (existT _ c d))) r) _ _ _) + (existT _ a (existT _ b (existT _ c d)))). +Defined. +End Fix3. + +End Wf. + +End Common. + +End ADTSynthesis. + +End ADTSynthesis_DOT_Common_DOT_Wf. + +Module Export ADTSynthesis_DOT_Parsers_DOT_StringLike_DOT_Core. +Module Export ADTSynthesis. +Module Export Parsers. +Module Export StringLike. +Module Export Core. +Import Coq.Setoids.Setoid. +Import Coq.Classes.Morphisms. + + + +Module Export StringLike. + Class StringLike {Char : Type} := + { + String :> Type; + is_char : String -> Char -> bool; + length : String -> nat; + take : nat -> String -> String; + drop : nat -> String -> String; + bool_eq : String -> String -> bool; + beq : relation String := fun x y => bool_eq x y + }. + + Arguments StringLike : clear implicits. + Infix "=s" := (@beq _ _) (at level 70, no associativity) : type_scope. + Notation "s ~= [ ch ]" := (is_char s ch) (at level 70, no associativity) : string_like_scope. + Local Open Scope string_like_scope. + + Definition str_le `{StringLike Char} (s1 s2 : String) + := length s1 < length s2 \/ s1 =s s2. + Infix "≤s" := str_le (at level 70, right associativity). + + Class StringLikeProperties (Char : Type) `{StringLike Char} := + { + singleton_unique : forall s ch ch', s ~= [ ch ] -> s ~= [ ch' ] -> ch = ch'; + length_singleton : forall s ch, s ~= [ ch ] -> length s = 1; + bool_eq_char : forall s s' ch, s ~= [ ch ] -> s' ~= [ ch ] -> s =s s'; + is_char_Proper :> Proper (beq ==> eq ==> eq) is_char; + length_Proper :> Proper (beq ==> eq) length; + take_Proper :> Proper (eq ==> beq ==> beq) take; + drop_Proper :> Proper (eq ==> beq ==> beq) drop; + bool_eq_Equivalence :> Equivalence beq; + bool_eq_empty : forall str str', length str = 0 -> length str' = 0 -> str =s str'; + take_short_length : forall str n, n <= length str -> length (take n str) = n; + take_long : forall str n, length str <= n -> take n str =s str; + take_take : forall str n m, take n (take m str) =s take (min n m) str; + drop_length : forall str n, length (drop n str) = length str - n; + drop_0 : forall str, drop 0 str =s str; + drop_drop : forall str n m, drop n (drop m str) =s drop (n + m) str; + drop_take : forall str n m, drop n (take m str) =s take (m - n) (drop n str); + take_drop : forall str n m, take n (drop m str) =s drop m (take (n + m) str) + }. + + Arguments StringLikeProperties Char {_}. +End StringLike. + +End Core. + +End StringLike. + +End Parsers. + +End ADTSynthesis. + +End ADTSynthesis_DOT_Parsers_DOT_StringLike_DOT_Core. + +Module Export ADTSynthesis. +Module Export Parsers. +Module Export ContextFreeGrammar. +Require Import Coq.Strings.String. +Require Import Coq.Lists.List. +Export ADTSynthesis.Parsers.StringLike.Core. +Import ADTSynthesis.Common. + +Local Open Scope string_like_scope. + +Section cfg. + Context {Char : Type}. + + Section definitions. + + Inductive item := + | Terminal (_ : Char) + | NonTerminal (_ : string). + + Definition production := list item. + Definition productions := list production. + + Record grammar := + { + Start_symbol :> string; + Lookup :> string -> productions; + Start_productions :> productions := Lookup Start_symbol; + Valid_nonterminals : list string; + Valid_productions : list productions := map Lookup Valid_nonterminals + }. + End definitions. + + Section parse. + Context {HSL : StringLike Char}. + Variable G : grammar. + + Inductive parse_of (str : String) : productions -> Type := + | ParseHead : forall pat pats, parse_of_production str pat + -> parse_of str (pat::pats) + | ParseTail : forall pat pats, parse_of str pats + -> parse_of str (pat::pats) + with parse_of_production (str : String) : production -> Type := + | ParseProductionNil : length str = 0 -> parse_of_production str nil + | ParseProductionCons : forall n pat pats, + parse_of_item (take n str) pat + -> parse_of_production (drop n str) pats + -> parse_of_production str (pat::pats) + with parse_of_item (str : String) : item -> Type := + | ParseTerminal : forall ch, str ~= [ ch ] -> parse_of_item str (Terminal ch) + | ParseNonTerminal : forall nt, parse_of str (Lookup G nt) + -> parse_of_item str (NonTerminal nt). + End parse. +End cfg. + +Arguments item _ : clear implicits. +Arguments production _ : clear implicits. +Arguments productions _ : clear implicits. +Arguments grammar _ : clear implicits. + +End ContextFreeGrammar. + +Module Export BaseTypes. + +Section recursive_descent_parser. + + Class parser_computational_predataT := + { nonterminals_listT : Type; + initial_nonterminals_data : nonterminals_listT; + is_valid_nonterminal : nonterminals_listT -> String.string -> bool; + remove_nonterminal : nonterminals_listT -> String.string -> nonterminals_listT; + nonterminals_listT_R : nonterminals_listT -> nonterminals_listT -> Prop; + remove_nonterminal_dec : forall ls nonterminal, + is_valid_nonterminal ls nonterminal + -> nonterminals_listT_R (remove_nonterminal ls nonterminal) ls; + ntl_wf : well_founded nonterminals_listT_R }. + + Class parser_removal_dataT' `{predata : parser_computational_predataT} := + { remove_nonterminal_1 + : forall ls ps ps', + is_valid_nonterminal (remove_nonterminal ls ps) ps' + -> is_valid_nonterminal ls ps'; + remove_nonterminal_2 + : forall ls ps ps', + is_valid_nonterminal (remove_nonterminal ls ps) ps' = false + <-> is_valid_nonterminal ls ps' = false \/ ps = ps' }. +End recursive_descent_parser. + +End BaseTypes. +Import Coq.Lists.List. +Import ADTSynthesis.Parsers.ContextFreeGrammar. + +Local Open Scope string_like_scope. + +Section cfg. + Context {Char} {HSL : StringLike Char} {G : grammar Char}. + Context {predata : @parser_computational_predataT} + {rdata' : @parser_removal_dataT' predata}. + + Inductive minimal_parse_of + : forall (str0 : String) (valid : nonterminals_listT) + (str : String), + productions Char -> Type := + | MinParseHead : forall str0 valid str pat pats, + @minimal_parse_of_production str0 valid str pat + -> @minimal_parse_of str0 valid str (pat::pats) + | MinParseTail : forall str0 valid str pat pats, + @minimal_parse_of str0 valid str pats + -> @minimal_parse_of str0 valid str (pat::pats) + with minimal_parse_of_production + : forall (str0 : String) (valid : nonterminals_listT) + (str : String), + production Char -> Type := + | MinParseProductionNil : forall str0 valid str, + length str = 0 + -> @minimal_parse_of_production str0 valid str nil + | MinParseProductionCons : forall str0 valid str n pat pats, + str ≤s str0 + -> @minimal_parse_of_item str0 valid (take n str) pat + -> @minimal_parse_of_production str0 valid (drop n str) pats + -> @minimal_parse_of_production str0 valid str (pat::pats) + with minimal_parse_of_item + : forall (str0 : String) (valid : nonterminals_listT) + (str : String), + item Char -> Type := + | MinParseTerminal : forall str0 valid str ch, + str ~= [ ch ] + -> @minimal_parse_of_item str0 valid str (Terminal ch) + | MinParseNonTerminal + : forall str0 valid str (nt : String.string), + @minimal_parse_of_nonterminal str0 valid str nt + -> @minimal_parse_of_item str0 valid str (NonTerminal nt) + with minimal_parse_of_nonterminal + : forall (str0 : String) (valid : nonterminals_listT) + (str : String), + String.string -> Type := + | MinParseNonTerminalStrLt + : forall str0 valid (nt : String.string) str, + length str < length str0 + -> is_valid_nonterminal initial_nonterminals_data nt + -> @minimal_parse_of str initial_nonterminals_data str (Lookup G nt) + -> @minimal_parse_of_nonterminal str0 valid str nt + | MinParseNonTerminalStrEq + : forall str0 str valid nonterminal, + str =s str0 + -> is_valid_nonterminal initial_nonterminals_data nonterminal + -> is_valid_nonterminal valid nonterminal + -> @minimal_parse_of str0 (remove_nonterminal valid nonterminal) str (Lookup G nonterminal) + -> @minimal_parse_of_nonterminal str0 valid str nonterminal. +End cfg. +Import ADTSynthesis.Common. + +Section general. + Context {Char} {HSL : StringLike Char} {G : grammar Char}. + + Class boolean_parser_dataT := + { predata :> parser_computational_predataT; + split_string_for_production + : item Char -> production Char -> String -> list nat }. + + Global Coercion predata : boolean_parser_dataT >-> parser_computational_predataT. + + Definition split_list_completeT `{data : @parser_computational_predataT} + {str0 valid} + (it : item Char) (its : production Char) + (str : String) + (pf : str ≤s str0) + (split_list : list nat) + + := ({ n : nat + & (minimal_parse_of_item (G := G) (predata := data) str0 valid (take n str) it) + * (minimal_parse_of_production (G := G) str0 valid (drop n str) its) }%type) + -> ({ n : nat + & (In n split_list) + * (minimal_parse_of_item (G := G) str0 valid (take n str) it) + * (minimal_parse_of_production (G := G) str0 valid (drop n str) its) }%type). + + Class boolean_parser_completeness_dataT' `{data : boolean_parser_dataT} := + { split_string_for_production_complete + : forall str0 valid str (pf : str ≤s str0) nt, + is_valid_nonterminal initial_nonterminals_data nt + -> ForallT + (Forall_tails + (fun prod + => match prod return Type with + | nil => True + | it::its + => @split_list_completeT data str0 valid it its str pf (split_string_for_production it its str) + end)) + (Lookup G nt) }. +End general. + +Module Export BooleanRecognizer. +Import Coq.Numbers.Natural.Peano.NPeano. +Import Coq.Arith.Compare_dec. +Import Coq.Arith.Wf_nat. + +Section recursive_descent_parser. + Context {Char} {HSL : StringLike Char} {HSLP : StringLikeProperties Char} {G : grammar Char}. + Context {data : @boolean_parser_dataT Char _}. + + Section bool. + Section parts. +Definition parse_item + (str_matches_nonterminal : String.string -> bool) + (str : String) + (it : item Char) + : bool. +Admitted. + + Section production. + Context {str0} + (parse_nonterminal + : forall (str : String), + str ≤s str0 + -> String.string + -> bool). + + Fixpoint parse_production + (str : String) + (pf : str ≤s str0) + (prod : production Char) + : bool. + Proof. + refine + match prod with + | nil => + + Nat.eq_dec (length str) 0 + | it::its + => let parse_production' := fun str pf => parse_production str pf its in + fold_right + orb + false + (map (fun n => + (parse_item + (parse_nonterminal (str := take n str) _) + (take n str) + it) + && parse_production' (drop n str) _)%bool + (split_string_for_production it its str)) + end; + revert pf; clear -HSLP; intros; admit. + Defined. + End production. + + Section productions. + Context {str0} + (parse_nonterminal + : forall (str : String) + (pf : str ≤s str0), + String.string -> bool). +Definition parse_productions + (str : String) + (pf : str ≤s str0) + (prods : productions Char) + : bool. +exact (fold_right orb + false + (map (parse_production parse_nonterminal pf) + prods)). +Defined. + End productions. + + Section nonterminals. + Section step. + Context {str0 valid} + (parse_nonterminal + : forall (p : String * nonterminals_listT), + prod_relation (ltof _ length) nonterminals_listT_R p (str0, valid) + -> forall str : String, + str ≤s fst p -> String.string -> bool). + + Definition parse_nonterminal_step + (str : String) + (pf : str ≤s str0) + (nt : String.string) + : bool. + Proof. + refine + (if lt_dec (length str) (length str0) + then + parse_productions + (@parse_nonterminal + (str : String, initial_nonterminals_data) + (or_introl _)) + (or_intror (reflexivity _)) + (Lookup G nt) + else + if Sumbool.sumbool_of_bool (is_valid_nonterminal valid nt) + then + parse_productions + (@parse_nonterminal + (str0 : String, remove_nonterminal valid nt) + (or_intror (conj eq_refl (remove_nonterminal_dec _ nt _)))) + (str := str) + _ + (Lookup G nt) + else + false); + assumption. + Defined. + End step. + + Section wf. +Definition parse_nonterminal_or_abort + : forall (p : String * nonterminals_listT) + (str : String), + str ≤s fst p + -> String.string + -> bool. +exact (Fix3 + _ _ _ + (well_founded_prod_relation + (well_founded_ltof _ length) + ntl_wf) + _ + (fun sl => @parse_nonterminal_step (fst sl) (snd sl))). +Defined. +Definition parse_nonterminal + (str : String) + (nt : String.string) + : bool. +exact (@parse_nonterminal_or_abort + (str : String, initial_nonterminals_data) str + (or_intror (reflexivity _)) nt). +Defined. + End wf. + End nonterminals. + End parts. + End bool. +End recursive_descent_parser. + +Section cfg. + Context {Char} {HSL : StringLike Char} {HSLP : @StringLikeProperties Char HSL} (G : grammar Char). + + Section definitions. + Context (P : String -> String.string -> Type). + + Definition Forall_parse_of_item' + (Forall_parse_of : forall {str pats} (p : parse_of G str pats), Type) + {str it} (p : parse_of_item G str it) + := match p return Type with + | ParseTerminal ch pf => unit + | ParseNonTerminal nt p' + => (P str nt * Forall_parse_of p')%type + end. + + Fixpoint Forall_parse_of {str pats} (p : parse_of G str pats) + := match p with + | ParseHead pat pats p' + => Forall_parse_of_production p' + | ParseTail _ _ p' + => Forall_parse_of p' + end + with Forall_parse_of_production {str pat} (p : parse_of_production G str pat) + := match p return Type with + | ParseProductionNil pf => unit + | ParseProductionCons pat strs pats p' p'' + => (Forall_parse_of_item' (@Forall_parse_of) p' * Forall_parse_of_production p'')%type + end. + + Definition Forall_parse_of_item {str it} (p : parse_of_item G str it) + := @Forall_parse_of_item' (@Forall_parse_of) str it p. + End definitions. + + End cfg. + +Section recursive_descent_parser_list. + Context {Char} {HSL : StringLike Char} {HLSP : StringLikeProperties Char} {G : grammar Char}. +Definition rdp_list_nonterminals_listT : Type. +exact (list String.string). +Defined. +Definition rdp_list_is_valid_nonterminal : rdp_list_nonterminals_listT -> String.string -> bool. +admit. +Defined. +Definition rdp_list_remove_nonterminal : rdp_list_nonterminals_listT -> String.string -> rdp_list_nonterminals_listT. +admit. +Defined. +Definition rdp_list_nonterminals_listT_R : rdp_list_nonterminals_listT -> rdp_list_nonterminals_listT -> Prop. +exact (ltof _ (@List.length _)). +Defined. + Lemma rdp_list_remove_nonterminal_dec : forall ls prods, + @rdp_list_is_valid_nonterminal ls prods = true + -> @rdp_list_nonterminals_listT_R (@rdp_list_remove_nonterminal ls prods) ls. +admit. +Defined. + Lemma rdp_list_ntl_wf : well_founded rdp_list_nonterminals_listT_R. + Proof. + unfold rdp_list_nonterminals_listT_R. + intro. + apply well_founded_ltof. + Defined. + + Global Instance rdp_list_predata : parser_computational_predataT + := { nonterminals_listT := rdp_list_nonterminals_listT; + initial_nonterminals_data := Valid_nonterminals G; + is_valid_nonterminal := rdp_list_is_valid_nonterminal; + remove_nonterminal := rdp_list_remove_nonterminal; + nonterminals_listT_R := rdp_list_nonterminals_listT_R; + remove_nonterminal_dec := rdp_list_remove_nonterminal_dec; + ntl_wf := rdp_list_ntl_wf }. +End recursive_descent_parser_list. + +Section sound. + Section general. + Context {Char} {HSL : StringLike Char} {HSLP : StringLikeProperties Char} (G : grammar Char). + Context {data : @boolean_parser_dataT Char _} + {cdata : @boolean_parser_completeness_dataT' Char _ G data} + {rdata : @parser_removal_dataT' predata}. + + Section parts. + + Section nonterminals. + Section wf. + + Lemma parse_nonterminal_sound + (str : String) (nonterminal : String.string) + : parse_nonterminal (G := G) str nonterminal + = true + -> parse_of_item G str (NonTerminal nonterminal). +admit. +Defined. + End wf. + End nonterminals. + End parts. + End general. +End sound. + +Import Coq.Strings.String. +Import ADTSynthesis.Parsers.ContextFreeGrammar. + +Fixpoint list_to_productions {T} (default : T) (ls : list (string * T)) : string -> T + := match ls with + | nil => fun _ => default + | (str, t)::ls' => fun s => if string_dec str s + then t + else list_to_productions default ls' s + end. + +Fixpoint list_to_grammar {T} (default : productions T) (ls : list (string * productions T)) : grammar T + := {| Start_symbol := hd ""%string (map (@fst _ _) ls); + Lookup := list_to_productions default ls; + Valid_nonterminals := map (@fst _ _) ls |}. + +Section interface. + Context {Char} (G : grammar Char). +Definition production_is_reachable (p : production Char) : Prop. +admit. +Defined. +Definition split_list_is_complete `{HSL : StringLike Char} (str : String) (it : item Char) (its : production Char) + (splits : list nat) + : Prop. +exact (forall n, + n <= length str + -> parse_of_item G (take n str) it + -> parse_of_production G (drop n str) its + -> production_is_reachable (it::its) + -> List.In n splits). +Defined. + + Record Splitter := + { + string_type :> StringLike Char; + splits_for : String -> item Char -> production Char -> list nat; + + string_type_properties :> StringLikeProperties Char; + splits_for_complete : forall str it its, + split_list_is_complete str it its (splits_for str it its) + + }. + Global Existing Instance string_type_properties. + + Record Parser (HSL : StringLike Char) := + { + has_parse : @String Char HSL -> bool; + + has_parse_sound : forall str, + has_parse str = true + -> parse_of_item G str (NonTerminal (Start_symbol G)); + + has_parse_complete : forall str (p : parse_of_item G str (NonTerminal (Start_symbol G))), + Forall_parse_of_item + (fun _ nt => List.In nt (Valid_nonterminals G)) + p + -> has_parse str = true + }. +End interface. + +Module Export ParserImplementation. + +Section implementation. + Context {Char} {G : grammar Char}. + Context (splitter : Splitter G). + + Local Instance parser_data : @boolean_parser_dataT Char _ := + { predata := rdp_list_predata (G := G); + split_string_for_production it its str + := splits_for splitter str it its }. + + Program Definition parser : Parser G splitter + := {| has_parse str := parse_nonterminal (G := G) (data := parser_data) str (Start_symbol G); + has_parse_sound str Hparse := parse_nonterminal_sound G _ _ Hparse; + has_parse_complete str p Hp := _ |}. + Next Obligation. +admit. +Defined. +End implementation. + +End ParserImplementation. + +Section implementation. + Context {Char} {ls : list (String.string * productions Char)}. + Local Notation G := (list_to_grammar (nil::nil) ls) (only parsing). + Context (splitter : Splitter G). + + Local Instance parser_data : @boolean_parser_dataT Char _ := parser_data splitter. + + Goal forall str : @String Char splitter, + let G' := + @BooleanRecognizer.parse_nonterminal Char splitter splitter G parser_data str G = true in + G'. + intros str G'. + Timeout 1 assert (pf' : G' -> Prop) by abstract admit. diff --git a/test-suite/bugs/closed/4653.v b/test-suite/bugs/closed/4653.v new file mode 100644 index 0000000000..4514342c5e --- /dev/null +++ b/test-suite/bugs/closed/4653.v @@ -0,0 +1,3 @@ +Definition T := Type. +Module Type S. Parameter foo : let A := T in True. End S. +Module M <: S. Lemma foo (A := T) : True. Proof I. End M. diff --git a/test-suite/bugs/closed/4673.v b/test-suite/bugs/closed/4673.v new file mode 100644 index 0000000000..1ae5081851 --- /dev/null +++ b/test-suite/bugs/closed/4673.v @@ -0,0 +1,57 @@ +(* -*- mode: coq; coq-prog-args: ("-emacs" "-R" "." "Fiat" "-top" "BooleanRecognizerOptimized" "-R" "." "Top") -*- *) +(* File reduced by coq-bug-finder from original input, then from 2407 lines to 22 lines, then from 528 lines to 35 lines, then from 331 lines to 42 lines, then from 56 lines to 42 lines, then from 63 lines to 46 lines, then from 60 lines to 46 lines *) (* coqc version 8.5 (February 2016) compiled on Feb 21 2016 15:26:16 with OCaml 4.02.3 + coqtop version 8.5 (February 2016) *) +Axiom proof_admitted : False. +Tactic Notation "admit" := case proof_admitted. +Require Coq.Lists.List. +Import Coq.Lists.List. +Import Coq.Classes.Morphisms. + +Definition list_caset A (P : list A -> Type) (N : P nil) (C : forall x xs, P (x::xs)) + ls + : P ls + := match ls with + | nil => N + | x::xs => C x xs + end. + +Global Instance list_caset_Proper' {A P} + : Proper (eq + ==> pointwise_relation _ (pointwise_relation _ eq) + ==> eq + ==> eq) + (@list_caset A (fun _ => P)). +admit. +Defined. + +Global Instance list_caset_Proper'' {A P} + : (Proper (eq ==> pointwise_relation _ (pointwise_relation _ eq) ==> forall_relation (fun _ => eq)) + (list_caset A (fun _ => P))). +Admitted. + +Goal forall (Char : Type) (P : forall _ : list bool, Prop) (l : list bool) (l0 : forall _ : forall _ : Char, bool, list bool) + + (T : Type) (T0 : forall _ : T, Type) (t : T), + + let predata := t in + + forall (splitdata : T0 predata) (l5 : forall _ : T0 t, list nat) (T1 : Type) (b : forall (_ : T1) (_ : Char), bool) + + (T2 : Type) (a11 : T2) (xs : list T2) (T3 : Type) (i0 : T3) (P0 : Set) (b1 : forall (_ : nat) (_ : P0), bool) + + (l2 : forall (_ : forall _ : T1, list bool) (_ : forall _ : P0, list bool) (_ : T2), list bool) + + (l1 : forall (_ : forall _ : forall _ : Char, bool, list bool) (_ : forall _ : P0, list bool) (_ : T3), list bool) + + (_ : forall NT : forall _ : P0, list bool, @eq (list bool) (l1 l0 NT i0) (l2 (fun f : T1 => l0 (b f)) NT a11)), + + P + (@list_caset T2 (fun _ : list T2 => list bool) l + (fun (_ : T2) (_ : list T2) => l1 l0 (fun a9 : P0 => @map nat bool (fun x0 : nat => b1 x0 a9) (l5 splitdata)) i0 +) xs). + intros. + subst predata; + let H := match goal with H : forall _, _ = _ |- _ => H end in + setoid_rewrite H || fail 0 "too early". + Undo. + setoid_rewrite H. diff --git a/test-suite/bugs/closed/4754.v b/test-suite/bugs/closed/4754.v new file mode 100644 index 0000000000..5bb3cd1be7 --- /dev/null +++ b/test-suite/bugs/closed/4754.v @@ -0,0 +1,35 @@ + +Require Import Coq.Setoids.Setoid Coq.Classes.Morphisms. +Definition f (v : option nat) := match v with + | Some k => Some k + | None => None + end. + +Axioms F G : (option nat -> option nat) -> Prop. +Axiom FG : forall f, f None = None -> F f = G f. + +Axiom admit : forall {T}, T. + +Existing Instance eq_Reflexive. + +Global Instance foo (A := nat) + : Proper ((pointwise_relation _ eq) + ==> eq ==> forall_relation (fun _ => Basics.flip Basics.impl)) + (@option_rect A (fun _ => Prop)) | 0. +exact admit. +Qed. + +Global Instance bar (A := nat) + : Proper ((pointwise_relation _ eq) + ==> eq ==> eq ==> Basics.flip Basics.impl) + (@option_rect A (fun _ => Prop)) | 0. +exact admit. +Qed. + +Goal forall k, option_rect (fun _ => Prop) (fun v : nat => v = v /\ F f) True k. +Proof. + intro. + pose proof (_ : (Proper (_ ==> eq ==> _) and)). + setoid_rewrite (FG _ _); [ | reflexivity.. ]. + Undo. + setoid_rewrite (FG _ eq_refl). (* Error: Tactic failure: setoid rewrite failed: Nothing to rewrite. in 8.5 *) Admitted.
\ No newline at end of file diff --git a/test-suite/bugs/closed/4769.v b/test-suite/bugs/closed/4769.v new file mode 100644 index 0000000000..d87906f313 --- /dev/null +++ b/test-suite/bugs/closed/4769.v @@ -0,0 +1,94 @@ + +(* -*- mode: coq; coq-prog-args: ("-emacs" "-nois" "-R" "." "Top" "-top" "bug_hom_anom_10") -*- *) +(* File reduced by coq-bug-finder from original input, then from 156 lines to 41 lines, then from 237 lines to 45 lines, then from 163 lines to 66 lines, then from 342 lines to 121 lines, then from 353 lines to 184 lines, then from 343 lines to 255 lines, then from 435 lines to 322 lines, then from 475 lines to 351 lines, then from 442 lines to 377 lines, then from 505 lines to 410 lines, then from 591 lines to 481 lines, then from 596 lines to 535 lines, then from 647 lines to 570 lines, then from 669 lines to 596 lines, then from 687 lines to 620 lines, then from 728 lines to 652 lines, then from 1384 lines to 683 lines, then from 984 lines to 707 lines, then from 1124 lines to 734 lines, then from 775 lines to 738 lines, then from 950 lines to 763 lines, then from 857 lines to 798 lines, then from 983 lines to 752 lines, then from 1598 lines to 859 lines, then from 873 lines to 859 lines, then from 875 lines to 862 lines, then from 901 lines to 863 lines, then from 1047 lines to 865 lines, then from 929 lines to 871 lines, then from 989 lines to 884 lines, then from 900 lines to 884 lines, then from 884 lines to 751 lines, then from 763 lines to 593 lines, then from 482 lines to 232 lines, then from 416 lines to 227 lines, then from 290 lines to 231 lines, then from 348 lines to 235 lines, then from 249 lines to 235 lines, then from 249 lines to 172 lines, then from 186 lines to 172 lines, then from 140 lines to 113 lines, then from 127 lines to 113 lines *) (* coqc version trunk (June 2016) compiled on Jun 2 2016 10:16:20 with OCaml 4.02.3 + coqtop version trunk (June 2016) *) + +Reserved Notation "x -> y" (at level 99, right associativity, y at level 200). +Reserved Notation "x * y" (at level 40, left associativity). +Delimit Scope type_scope with type. +Open Scope type_scope. +Global Set Universe Polymorphism. +Notation "A -> B" := (forall (_ : A), B) : type_scope. +Set Implicit Arguments. +Global Set Nonrecursive Elimination Schemes. +Record prod (A B : Type) := pair { fst : A ; snd : B }. +Notation "x * y" := (prod x y) : type_scope. +Axiom admit : forall {T}, T. +Delimit Scope function_scope with function. +Notation compose := (fun g f x => g (f x)). +Notation "g 'o' f" := (compose g%function f%function) (at level 40, left associativity) : function_scope. +Record PreCategory := + Build_PreCategory { + object :> Type; + morphism : object -> object -> Type; + identity : forall x, morphism x x }. +Bind Scope category_scope with PreCategory. +Record Functor (C D : PreCategory) := { object_of :> C -> D }. +Bind Scope functor_scope with Functor. +Class Isomorphic {C : PreCategory} (s d : C) := {}. +Definition oppositeC (C : PreCategory) : PreCategory + := @Build_PreCategory C (fun s d => morphism C d s) admit. +Notation "C ^op" := (oppositeC C) (at level 3, format "C '^op'") : category_scope. +Definition oppositeF C D (F : Functor C D) : Functor C^op D^op + := Build_Functor (C^op) (D^op) (object_of F). +Definition set_cat : PreCategory := @Build_PreCategory Type (fun x y => x -> y) admit. +Definition prodC (C D : PreCategory) : PreCategory + := @Build_PreCategory + (C * D)%type + (fun s d => (morphism C (fst s) (fst d) + * morphism D (snd s) (snd d))%type) + admit. +Infix "*" := prodC : category_scope. +Section composition. + Variables B C D E : PreCategory. + Definition composeF (G : Functor D E) (F : Functor C D) : Functor C E := Build_Functor C E (fun c => G (F c)). +End composition. +Infix "o" := composeF : functor_scope. +Definition fstF {C D} : Functor (C * D) C := admit. +Definition sndF {C D} : Functor (C * D) D := admit. +Definition prodF C D D' (F : Functor C D) (F' : Functor C D') : Functor C (D * D') := admit. +Local Infix "*" := prodF : functor_scope. +Definition pairF C D C' D' (F : Functor C D) (F' : Functor C' D') : Functor (C * C') (D * D') + := (F o fstF) * (F' o sndF). +Section hom_functor. + Variable C : PreCategory. + Local Notation obj_of c'c := + ((morphism + C + (fst (c'c : object (C^op * C))) + (snd (c'c : object (C^op * C))))). + Definition hom_functor : Functor (C^op * C) set_cat + := Build_Functor (C^op * C) set_cat (fun c'c => obj_of c'c). +End hom_functor. +Definition identityF C : Functor C C := admit. +Definition functor_category (C D : PreCategory) : PreCategory + := @Build_PreCategory (Functor C D) admit admit. +Local Notation "C -> D" := (functor_category C D) : category_scope. +Definition NaturalIsomorphism (C D : PreCategory) F G := @Isomorphic (C -> D) F G. + +Section Adjunction. + Variables C D : PreCategory. + Variable F : Functor C D. + Variable G : Functor D C. + + Record AdjunctionHom := + { + mate_of : @NaturalIsomorphism + (prodC (oppositeC C) D) + (@set_cat) + (@composeF + (prodC (oppositeC C) D) + (prodC (oppositeC D) D) + (@set_cat) (@hom_functor D) + (@pairF (oppositeC C) + (oppositeC D) D D + (@oppositeF C D F) (identityF D))) + (@composeF + (prodC (oppositeC C) D) + (prodC (oppositeC C) C) + (@set_cat) (@hom_functor C) + (@pairF (oppositeC C) + (oppositeC C) D C + (identityF (oppositeC C)) G)) + }. +End Adjunction.
\ No newline at end of file diff --git a/test-suite/success/Case13.v b/test-suite/success/Case13.v index f14725a8ee..8f95484cfd 100644 --- a/test-suite/success/Case13.v +++ b/test-suite/success/Case13.v @@ -55,6 +55,14 @@ Check (fun x : I' 0 => match x with | _ => 0 end). +(* This one could eventually be solved, the "Fail" is just to ensure *) +(* that it does not fail with an anomaly, as it did at some time *) +Fail Check (fun x : I' 0 => match x return _ x with + | C2' _ _ => 0 + | niln => 0 + | _ => 0 + end). + (* Check insertion of coercions around matched subterm *) Parameter A:Set. diff --git a/test-suite/success/programequality.v b/test-suite/success/programequality.v new file mode 100644 index 0000000000..414c572f81 --- /dev/null +++ b/test-suite/success/programequality.v @@ -0,0 +1,13 @@ +Require Import Program. + +Axiom t : nat -> Set. + +Goal forall (x y : nat) (e : x = y) (e' : x = y) (P : t y -> x = y -> Type) + (a : t x), + P (eq_rect _ _ a _ e) e'. +Proof. + intros. + pi_eq_proofs. clear e. + destruct e'. simpl. + change (P a eq_refl). +Abort.
\ No newline at end of file diff --git a/theories/Classes/Equivalence.v b/theories/Classes/Equivalence.v index c458894795..80b0b7e4c6 100644 --- a/theories/Classes/Equivalence.v +++ b/theories/Classes/Equivalence.v @@ -49,11 +49,11 @@ Infix "=~=" := pequiv (at level 70, no associativity) : equiv_scope. (** Shortcuts to make proof search easier. *) -Program Instance equiv_reflexive `(sa : Equivalence A) : Reflexive equiv. +Program Instance equiv_reflexive `(sa : Equivalence A) : Reflexive equiv | 1. -Program Instance equiv_symmetric `(sa : Equivalence A) : Symmetric equiv. +Program Instance equiv_symmetric `(sa : Equivalence A) : Symmetric equiv | 1. -Program Instance equiv_transitive `(sa : Equivalence A) : Transitive equiv. +Program Instance equiv_transitive `(sa : Equivalence A) : Transitive equiv | 1. Next Obligation. Proof. intros A R sa x y z Hxy Hyz. @@ -123,7 +123,7 @@ Section Respecting. End Respecting. -(** The default equivalence on function spaces, with higher-priority than [eq]. *) +(** The default equivalence on function spaces, with higher priority than [eq]. *) Instance pointwise_reflexive {A} `(reflb : Reflexive B eqB) : Reflexive (pointwise_relation A eqB) | 9. diff --git a/theories/Program/Equality.v b/theories/Program/Equality.v index a349eb9085..d6f9bb9df0 100644 --- a/theories/Program/Equality.v +++ b/theories/Program/Equality.v @@ -8,7 +8,6 @@ (** Tactics related to (dependent) equality and proof irrelevance. *) -Require Export ProofIrrelevance. Require Export JMeq. Require Import Coq.Program.Tactics. @@ -143,7 +142,7 @@ Ltac pi_eq_proof_hyp p := | [ H : X = Y |- _ ] => match p with | H => fail 2 - | _ => rewrite (proof_irrelevance (X = Y) p H) + | _ => rewrite (UIP _ X Y p H) end | _ => fail " No hypothesis with same type " end @@ -166,7 +165,7 @@ Hint Rewrite <- eq_rect_eq : refl_id. [coerce_* t eq_refl = t]. *) Lemma JMeq_eq_refl {A} (x : A) : JMeq_eq (@JMeq_refl _ x) = eq_refl. -Proof. apply proof_irrelevance. Qed. +Proof. apply UIP. Qed. Lemma UIP_refl_refl A (x : A) : Eqdep.EqdepTheory.UIP_refl A x eq_refl = eq_refl. diff --git a/theories/Program/Subset.v b/theories/Program/Subset.v index c8f37318d1..2a3ec926b2 100644 --- a/theories/Program/Subset.v +++ b/theories/Program/Subset.v @@ -9,6 +9,7 @@ Require Import Coq.Program.Utils. Require Import Coq.Program.Equality. +Require Export ProofIrrelevance. Local Open Scope program_scope. diff --git a/theories/Reals/Sqrt_reg.v b/theories/Reals/Sqrt_reg.v index 10527442e8..d43baee8cd 100644 --- a/theories/Reals/Sqrt_reg.v +++ b/theories/Reals/Sqrt_reg.v @@ -339,7 +339,7 @@ Proof. rewrite <- H1; rewrite sqrt_0; unfold Rminus; rewrite Ropp_0; rewrite Rplus_0_r; rewrite <- H1 in H5; unfold Rminus in H5; rewrite Ropp_0 in H5; rewrite Rplus_0_r in H5. - destruct (Rcase_abs x0) as [Hlt|Hgt]_eqn:Heqs. + destruct (Rcase_abs x0) as [Hlt|Hgt] eqn:Heqs. unfold sqrt. rewrite Heqs. rewrite Rabs_R0; apply H2. rewrite Rabs_right. diff --git a/tools/coq_makefile.ml b/tools/coq_makefile.ml index b86df7c80e..ac69a69a4a 100644 --- a/tools/coq_makefile.ml +++ b/tools/coq_makefile.ml @@ -582,7 +582,7 @@ let parameters () = print "define donewline\n\n\nendef\n"; print "includecmdwithout@ = $(eval $(subst @,$(donewline),$(shell { $(1) | tr -d '\\r' | tr '\\n' '@'; })))\n"; print "$(call includecmdwithout@,$(COQBIN)coqtop -config)\n\n"; - print "TIMED?=\nTIMECMD?=\nSTDTIME=/usr/bin/time -f \"$* (user: %U mem: %M ko)\"\n"; + print "TIMED?=\nTIMECMD?=\nSTDTIME?=/usr/bin/time -f \"$* (user: %U mem: %M ko)\"\n"; print "TIMER=$(if $(TIMED), $(STDTIME), $(TIMECMD))\n\n"; print "vo_to_obj = $(addsuffix .o,\\\n"; print " $(filter-out Warning: Error:,\\\n"; diff --git a/tools/coqdoc/cpretty.mll b/tools/coqdoc/cpretty.mll index 005ffdae72..919f37b91b 100644 --- a/tools/coqdoc/cpretty.mll +++ b/tools/coqdoc/cpretty.mll @@ -675,7 +675,7 @@ and doc_bol = parse in match check_start_list line with | Neither -> backtrack_past_newline lexbuf; doc None lexbuf - | List n -> Output.paragraph (); + | List n -> if lines > 0 then Output.paragraph (); Output.item 1; doc (Some [n]) lexbuf | Rule -> Output.rule (); doc None lexbuf } @@ -736,24 +736,7 @@ and doc_list_bol indents = parse in let (n_spaces,_) = count_spaces buf in match find_level indents n_spaces with - | InLevel _ -> - Output.paragraph (); - backtrack_past_newline lexbuf; - doc_list_bol indents lexbuf - | StartLevel n -> - if n = 1 then - begin - Output.stop_item (); - backtrack_past_newline lexbuf; - doc_bol lexbuf - end - else - begin - Output.paragraph (); - backtrack_past_newline lexbuf; - doc_list_bol indents lexbuf - end - | Before -> + | StartLevel 1 | Before -> (* Here we were at the beginning of a line, and it was blank. The next line started before any list items. So: insert a paragraph for the empty line, rewind to whatever's just @@ -763,6 +746,10 @@ and doc_list_bol indents = parse Output.paragraph (); backtrack_past_newline lexbuf; doc_bol lexbuf + | StartLevel _ | InLevel _ -> + Output.paragraph (); + backtrack_past_newline lexbuf; + doc_list_bol indents lexbuf } | space* _ @@ -771,10 +758,7 @@ and doc_list_bol indents = parse | Before -> Output.stop_item (); backtrack lexbuf; doc_bol lexbuf | StartLevel n -> - (if n = 1 then - Output.stop_item () - else - Output.reach_item_level (n-1)); + Output.reach_item_level (n-1); backtrack lexbuf; doc (Some (take (n-1) indents)) lexbuf | InLevel (n,_) -> diff --git a/toplevel/command.ml b/toplevel/command.ml index f92ea027dd..097865648e 100644 --- a/toplevel/command.ml +++ b/toplevel/command.ml @@ -1251,6 +1251,11 @@ let out_def = function | Some def -> def | None -> error "Program Fixpoint needs defined bodies." +let collect_evars_of_term evd c ty = + let evars = Evar.Set.union (Evd.evars_of_term c) (Evd.evars_of_term ty) in + Evar.Set.fold (fun ev acc -> Evd.add acc ev (Evd.find_undefined evd ev)) + evars (Evd.from_ctx (Evd.evar_universe_context evd)) + let do_program_recursive local p fixkind fixl ntns = let isfix = fixkind != Obligations.IsCoFixpoint in let (env, rec_sign, pl, evd), fix, info = @@ -1268,8 +1273,9 @@ let do_program_recursive local p fixkind fixl ntns = and typ = nf_evar evd (Termops.it_mkNamedProd_or_LetIn typ rec_sign) in + let evm = collect_evars_of_term evd def typ in let evars, _, def, typ = - Obligations.eterm_obligations env id evd + Obligations.eterm_obligations env id evm (List.length rec_sign) def typ in (id, def, typ, imps, evars) in diff --git a/toplevel/coqtop.ml b/toplevel/coqtop.ml index d141cd8ec1..c49a97cadb 100644 --- a/toplevel/coqtop.ml +++ b/toplevel/coqtop.ml @@ -54,7 +54,7 @@ let init_color () = Terminal.has_style Unix.stderr && (* emacs compilation buffer does not support colors by default, its TERM variable is set to "dumb". *) - Unix.getenv "TERM" <> "dumb" + try Sys.getenv "TERM" <> "dumb" with Not_found -> false in if has_color then begin let colors = try Some (Sys.getenv "COQ_COLORS") with Not_found -> None in diff --git a/toplevel/himsg.ml b/toplevel/himsg.ml index b3eae3765b..ff4c18ad21 100644 --- a/toplevel/himsg.ml +++ b/toplevel/himsg.ml @@ -320,6 +320,7 @@ let explain_unification_error env sigma p1 p2 = function | CannotSolveConstraint ((pb,env,t,u),e) -> let t = Evarutil.nf_evar sigma t in let u = Evarutil.nf_evar sigma u in + let env = make_all_name_different env in (strbrk "cannot satisfy constraint " ++ pr_lconstr_env env sigma t ++ str " == " ++ pr_lconstr_env env sigma u) :: aux t u e |