- Fix handling of opaque polymorphic definitions which were turned transparent.

- Decomment code in reductionops forgotten after debugging.

2 files changed, 21 insertions, 18 deletions

diff --git a/kernel/term_typing.ml b/kernel/term_typing.ml
index c44adad5cb..da0326981c 100644
--- a/kernel/term_typing.ml
+++ b/kernel/term_typing.ml
@@ -202,7 +202,10 @@ let infer_declaration env kn dcl =
 	  let j = infer env body in
 	  let typ = constrain_type env j c.const_entry_polymorphic usubst (map_option_typ typ) in
 	  let def = hcons_constr (Vars.subst_univs_level_constr usubst j.uj_val) in
-	  let def = Def (Mod_subst.from_val def) in
+	  let def = 
+	    if opaque then OpaqueDef (Opaqueproof.create (Future.from_val (def, Univ.ContextSet.empty)))
+	    else Def (Mod_subst.from_val def) 
+	  in
 	    def, typ, None
       in
 	feedback_completion_typecheck feedback_id;
diff --git a/pretyping/reductionops.ml b/pretyping/reductionops.ml
index 1f3e7b5717..5ca61e3653 100644
--- a/pretyping/reductionops.ml
+++ b/pretyping/reductionops.ml
@@ -654,23 +654,23 @@ let reducible_mind_case c = match kind_of_term c with
 *)
 let magicaly_constant_of_fixbody env bd = function
   | Name.Anonymous -> bd
-  | Name.Name id -> bd
-    (* try *)
-    (*   let cst = Nametab.locate_constant *)
-    (* 	(Libnames.make_qualid DirPath.empty id) in *)
-    (*   let (cst, u), ctx = Universes.fresh_constant_instance env cst in *)
-    (*   match constant_opt_value_in env (cst,u) with *)
-    (*   | None -> bd *)
-    (*   | Some t ->  *)
-    (*     let b, csts = Universes.eq_constr_universes t bd in *)
-    (* 	let subst = Universes.Constraints.fold (fun (l,d,r) acc ->  *)
-    (* 	  Univ.LMap.add (Option.get (Universe.level l)) (Option.get (Universe.level r)) acc) *)
-    (* 	  csts Univ.LMap.empty *)
-    (* 	in *)
-    (* 	let inst = Instance.subst_fn (fun u -> Univ.LMap.find u subst) u in *)
-    (*       if b then mkConstU (cst,inst) else bd *)
-    (* with *)
-    (* | Not_found -> bd *)
+  | Name.Name id ->
+    try
+      let cst = Nametab.locate_constant
+    	(Libnames.make_qualid DirPath.empty id) in
+      let (cst, u), ctx = Universes.fresh_constant_instance env cst in
+      match constant_opt_value_in env (cst,u) with
+      | None -> bd
+      | Some t ->
+        let b, csts = Universes.eq_constr_universes t bd in
+    	let subst = Universes.Constraints.fold (fun (l,d,r) acc ->
+    	  Univ.LMap.add (Option.get (Universe.level l)) (Option.get (Universe.level r)) acc)
+    	  csts Univ.LMap.empty
+    	in
+    	let inst = Instance.subst_fn (fun u -> Univ.LMap.find u subst) u in
+          if b then mkConstU (cst,inst) else bd
+    with
+    | Not_found -> bd
 
 let contract_cofix ?env (bodynum,(names,types,bodies as typedbodies)) =
   let nbodies = Array.length bodies in