Contounement d'un probleme avec la VM dans Function

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9538 85f007b7-540e-0410-9357-904b9bb8a0f7

2 files changed, 36 insertions, 7 deletions

diff --git a/contrib/funind/functional_principles_types.ml b/contrib/funind/functional_principles_types.ml
index 8ad2e72bbf..cb804f6f2b 100644
--- a/contrib/funind/functional_principles_types.ml
+++ b/contrib/funind/functional_principles_types.ml
@@ -561,6 +561,15 @@ let make_scheme (fas : (constant*Rawterm.rawsort) list) : Entries.definition_ent
       (fun _ _ _ -> ())
   in      
   incr i;
+  let opacity = 
+    let finfos = find_Function_infos this_block_funs.(0) in 
+    try 
+      let equation =  out_some finfos.equation_lemma in  
+      (Global.lookup_constant equation).Declarations.const_opaque 
+    with Failure "out_some" -> (* non recursive definition *) 
+      false
+  in
+  let const = {const with const_entry_opaque = opacity } in 
   (* The others are just deduced *)
   if other_princ_types = [] 
   then
@@ -642,10 +651,12 @@ let build_scheme fas =
   in 
   List.iter2 
     (fun (princ_id,_,_) def_entry -> 
-       ignore (Declare.declare_constant 
-		 princ_id 
-		 (Entries.DefinitionEntry def_entry,Decl_kinds.IsProof Decl_kinds.Theorem));
-       Options.if_verbose (fun id -> Pp.msgnl (Ppconstr.pr_id id ++ str " is defined")) princ_id
+       ignore 
+	 (Declare.declare_constant 
+	    princ_id 
+	    (Entries.DefinitionEntry def_entry,Decl_kinds.IsProof Decl_kinds.Theorem));
+       Options.if_verbose 
+	 (fun id -> Pp.msgnl (Ppconstr.pr_id id ++ str " is defined")) princ_id
     )
     fas
     bodies_types
diff --git a/contrib/recdef/recdef.ml4 b/contrib/recdef/recdef.ml4
index 353fcdb3bb..8f598acd0b 100644
--- a/contrib/recdef/recdef.ml4
+++ b/contrib/recdef/recdef.ml4
@@ -850,6 +850,16 @@ let open_new_goal using_lemmas ref goal_name (gls_type,decompose_and_tac,nb_goal
   if occur_existential gls_type then
     Util.error "\"abstract\" cannot handle existentials";
   let hook _ _ = 
+    let opacity = 
+      let na_ref = Libnames.Ident (dummy_loc,na) in 
+      let na_global = Nametab.global na_ref in
+      match na_global with 
+	  ConstRef c -> 
+	    let cb = Global.lookup_constant c in 
+	    if cb.Declarations.const_opaque then true 
+	    else begin  match cb.const_body with None -> true | _ -> false end 
+	| _ -> anomaly "equation_lemma: not a constant"
+    in
     let lemma = mkConst (Lib.make_con na) in 
     Array.iteri 
       (fun i _ -> 
@@ -857,7 +867,7 @@ let open_new_goal using_lemmas ref goal_name (gls_type,decompose_and_tac,nb_goal
       (Array.make nb_goal ())
     ;
     ref := Some lemma ;
-    defined ();
+    Command.save_named opacity;
   in
   start_proof
     na
@@ -888,7 +898,7 @@ let open_new_goal using_lemmas ref goal_name (gls_type,decompose_and_tac,nb_goal
   with UserError _ -> 
     defined ()
   
-    
+;;    
 let com_terminate 
     tcc_lemma_name 
     tcc_lemma_ref 
@@ -1140,6 +1150,14 @@ let (com_eqn : identifier ->
        global_reference -> global_reference -> global_reference
 	 -> constr -> unit) =
   fun eq_name functional_ref f_ref terminate_ref equation_lemma_type ->
+    let opacity = 
+      match terminate_ref with 
+	| ConstRef c -> 	      
+	    let cb = Global.lookup_constant c in 
+	    if cb.Declarations.const_opaque then true 
+	    else begin match cb.const_body with None -> true | _ -> false end 
+	| _ -> anomaly "terminate_lemma: not a constant"
+    in 
     let (evmap, env) = Command.get_current_context() in
     let f_constr = (constr_of_reference f_ref) in
     let equation_lemma_type = subst1 f_constr equation_lemma_type in
@@ -1159,7 +1177,7 @@ let (com_eqn : identifier ->
 	       )
 	  )
        );
-     Options.silently defined (); 
+     Options.silently (fun () -> Command.save_named opacity) (); 
     );;