diff options
| author |  Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2016-08-17 16:17:17 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2016-08-17 16:17:17 +0200 |
| commit | 13fb26d615cdb03a4c4841c20b108deab2de60b3 (patch) | |
| tree | 55f86d47695ee2071d1f886ce70ad7eec6a1e866 /toplevel | |
| parent | 3fd0b8ad700bd77aabdd3f3f33b13ba5e93d8bc8 (diff) | |
| parent | bc7ffd368789cb82bb8fc8b642b3de870b92c897 (diff) | |
Merge branch 'v8.6'
Diffstat (limited to 'toplevel')
| -rw-r--r-- | toplevel/command.ml | 8 | ||||
| -rw-r--r-- | toplevel/coqtop.ml | 2 |
2 files changed, 8 insertions, 2 deletions
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 |