From 9f5e248704f1574b0acbb9bddd287e40daac8727 Mon Sep 17 00:00:00 2001 From: Matthieu Sozeau Date: Wed, 27 Jul 2016 18:26:42 +0200 Subject: Fix bug #3886, generation of obligations of fixes This partially reverts c14ccd1b8a3855d4eb369be311d4b36a355e46c1 --- toplevel/command.ml | 8 +++++++- 1 file changed, 7 insertions(+), 1 deletion(-) (limited to 'toplevel') diff --git a/toplevel/command.ml b/toplevel/command.ml index 8eb2232ed..b9e4dbd7b 100644 --- a/toplevel/command.ml +++ b/toplevel/command.ml @@ -1222,6 +1222,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 = @@ -1239,8 +1244,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 -- cgit v1.2.3 From c90c53129436014b0020c52641277d616144282a Mon Sep 17 00:00:00 2001 From: Guillaume Melquiond Date: Thu, 11 Aug 2016 09:37:29 +0200 Subject: Do not assume the "TERM" environment variable is always set (bug #5007). --- toplevel/coqtop.ml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'toplevel') diff --git a/toplevel/coqtop.ml b/toplevel/coqtop.ml index 9e1a76bbd..3d5080177 100644 --- a/toplevel/coqtop.ml +++ b/toplevel/coqtop.ml @@ -55,7 +55,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 -- cgit v1.2.3