diff options
37 files changed, 635 insertions, 217 deletions
@@ -85,13 +85,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 diff --git a/configure.ml b/configure.ml index 63cf138db..13e1daedc 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 feef80ed3..fcee79e07 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 b2eb280d6..d82fb74f2 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-oth.tex b/doc/refman/RefMan-oth.tex index 6a8bda35d..919e7b5cd 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 b63391913..bd86f4bd2 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 111d0f3e8..c0c81442d 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 196f44760..6ba8a5112 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 d6cf83525..942414511 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 129cb3868..638adea5d 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 c7b0bb5a5..9381a33af 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 aaf603efd..7473a251b 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 18557ab6b..50b3f2c0a 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 f0698a54a..fe69be9e4 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 3a33bbb1d..3241a962d 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 426b0a328..801869d1d 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 fb1baae0a..7c4688f9f 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) -> diff --git a/interp/notation_ops.ml b/interp/notation_ops.ml index 6478ade61..f3e0682bd 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/vconv.ml b/kernel/vconv.ml index c729a6ce2..894f5296a 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 602bba6a5..c8283e3c7 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 8dd24d278..7824506da 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/ltac/rewrite.ml b/ltac/rewrite.ml index e327deda0..47c78ae5c 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; diff --git a/plugins/extraction/modutil.ml b/plugins/extraction/modutil.ml index 864d90a0f..60fe8e762 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 5e43dfc42..187601fc6 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/detyping.ml b/pretyping/detyping.ml index d4066f387..85125a502 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 187eba16b..1ef96e034 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 0e4885bea..696d419af 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 99c2d8210..93073fdc7 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 4aa7ffa7b..2c97cf442 100644 --- a/tactics/equality.ml +++ b/tactics/equality.ml @@ -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/test-suite/bugs/closed/3070.v b/test-suite/bugs/closed/3070.v new file mode 100644 index 000000000..7a8feca58 --- /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 000000000..2ac4abe54 --- /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/4673.v b/test-suite/bugs/closed/4673.v new file mode 100644 index 000000000..1ae508185 --- /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 000000000..5bb3cd1be --- /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 000000000..d87906f31 --- /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/tools/coq_makefile.ml b/tools/coq_makefile.ml index b86df7c80..ac69a69a4 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/toplevel/command.ml b/toplevel/command.ml index f92ea027d..097865648 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 d141cd8ec..c49a97cad 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 |