From 4ae315f92e4a9849a56d3d9b0da33027f362d6e8 Mon Sep 17 00:00:00 2001
From: Matthieu Sozeau
Date: Thu, 26 May 2016 10:55:15 +0200
Subject: Univs/Program/Function: Fix bug #4725

- In Program, a check_evars_are_solved was introduced
too early. Program does it's checking of evars by itself.
- In Function, the universe environments were not threaded
correctly.
---
 plugins/funind/recdef.ml | 10 +++++-----
 1 file changed, 5 insertions(+), 5 deletions(-)

(limited to 'plugins')

diff --git a/plugins/funind/recdef.ml b/plugins/funind/recdef.ml
index 065d0fe537..bc8e721edc 100644
--- a/plugins/funind/recdef.ml
+++ b/plugins/funind/recdef.ml
@@ -1510,13 +1510,13 @@ let recursive_definition is_mes function_name rec_impls type_of_f r rec_arg_num
   let functional_id =  add_suffix function_name "_F" in
   let term_id = add_suffix function_name "_terminate" in
   let functional_ref = declare_fun functional_id (IsDefinition Decl_kinds.Definition) ~ctx:(snd (Evd.universe_context evm)) res in
+  (* Refresh the global universes, now including those of _F *)
+  let evm = Evd.from_env (Global.env ()) in
   let env_with_pre_rec_args = push_rel_context(List.map (function (x,t) -> (x,None,t)) pre_rec_args) env in  
-  let relation =
-    fst (*FIXME*)(interp_constr
-      env_with_pre_rec_args
-      (Evd.from_env env_with_pre_rec_args)
-      r)
+  let relation, evuctx =
+    interp_constr env_with_pre_rec_args evm r
   in
+  let evm = Evd.from_ctx evuctx in
   let tcc_lemma_name = add_suffix function_name "_tcc" in
   let tcc_lemma_constr = ref None in
   (* let _ = Pp.msgnl (str "relation := " ++ Printer.pr_lconstr_env env_with_pre_rec_args relation) in *)
-- 
cgit v1.2.3


From 4b4397e185cee54052819ad63bef3ecd56ba4512 Mon Sep 17 00:00:00 2001
From: Guillaume Melquiond
Date: Thu, 23 Jun 2016 10:30:04 +0200
Subject: Fix typo.

---
 plugins/extraction/extraction.ml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'plugins')

diff --git a/plugins/extraction/extraction.ml b/plugins/extraction/extraction.ml
index 0ac8e3c4cf..114c5149f6 100644
--- a/plugins/extraction/extraction.ml
+++ b/plugins/extraction/extraction.ml
@@ -36,7 +36,7 @@ let current_fixpoints = ref ([] : constant list)
 let none = Evd.empty
 
 (* NB: In OCaml, [type_of] and [get_of] might raise
-   [SingletonInductiveBecomeProp]. this exception will be catched
+   [SingletonInductiveBecomeProp]. This exception will be caught
    in late wrappers around the exported functions of this file,
    in order to display the location of the issue. *)
 
-- 
cgit v1.2.3