handling Functional Scheme for required but not imported modules

3 files changed, 29 insertions, 14 deletions

diff --git a/plugins/funind/glob_term_to_relation.ml b/plugins/funind/glob_term_to_relation.ml
index 5cbe32d59..a2577e2b0 100644
--- a/plugins/funind/glob_term_to_relation.ml
+++ b/plugins/funind/glob_term_to_relation.ml
@@ -1233,11 +1233,12 @@ let rec rebuild_return_type rt =
 
 
 let do_build_inductive
-    funnames (funsargs: (Name.t * glob_constr * bool) list list)
-    returned_types
-    (rtl:glob_constr list) =
+      mp_dp
+      funnames (funsargs: (Name.t * glob_constr * bool) list list)
+      returned_types
+      (rtl:glob_constr list) =
   let _time1 = System.get_time () in
-(*   Pp.msgnl (prlist_with_sep fnl Printer.pr_glob_constr rtl); *)
+  (*   Pp.msgnl (prlist_with_sep fnl Printer.pr_glob_constr rtl); *)
   let funnames_as_set = List.fold_right Id.Set.add funnames Id.Set.empty in
   let funnames = Array.of_list funnames in
   let funsargs = Array.of_list funsargs in
@@ -1254,7 +1255,17 @@ let do_build_inductive
   let env =
     Array.fold_right
       (fun id env ->
-	 Environ.push_named (id,None,Typing.type_of env Evd.empty (Constrintern.global_reference id))  env
+       let c =
+	 match mp_dp with
+	 | None -> (Constrintern.global_reference id)
+	 | Some(mp,dp) -> mkConst (make_con mp dp (Label.of_id id))
+       in
+       Environ.push_named (id,None,
+			   try
+			     Typing.type_of env Evd.empty c
+			   with Not_found ->
+			     raise (UserError("do_build_inductive", str "Cannot handle partial fixpoint"))
+			  )  env
       )
       funnames
       (Global.env ())
@@ -1450,9 +1461,9 @@ let do_build_inductive
 
 
 
-let build_inductive funnames funsargs returned_types rtl =
+let build_inductive mp_dp funnames funsargs returned_types rtl =
   try
-    do_build_inductive funnames funsargs returned_types rtl
+    do_build_inductive mp_dp funnames funsargs returned_types rtl
   with e when Errors.noncritical e -> raise (Building_graph e)
 
 
diff --git a/plugins/funind/glob_term_to_relation.mli b/plugins/funind/glob_term_to_relation.mli
index 101be24fd..b0a05ec32 100644
--- a/plugins/funind/glob_term_to_relation.mli
+++ b/plugins/funind/glob_term_to_relation.mli
@@ -7,6 +7,7 @@ open Names
 *)
 
 val build_inductive :
+  (ModPath.t * DirPath.t) option ->
   Id.t list -> (* The list of function name *)
   (Name.t*Glob_term.glob_constr*bool) list list -> (* The list of function args *)
   Constrexpr.constr_expr list -> (* The list of function returned type *)
diff --git a/plugins/funind/indfun.ml b/plugins/funind/indfun.ml
index d1747eed6..2ce9f4f61 100644
--- a/plugins/funind/indfun.ml
+++ b/plugins/funind/indfun.ml
@@ -291,7 +291,7 @@ let error_error names e =
 	     e_explain e)
     | _ -> raise e
 
-let generate_principle  on_error
+let generate_principle  mp_dp on_error
     is_general do_built (fix_rec_l:(Vernacexpr.fixpoint_expr * Vernacexpr.decl_notation list) list) recdefs  interactive_proof
     (continue_proof : int -> Names.constant array -> Term.constr array -> int ->
       Tacmach.tactic) : unit =
@@ -301,7 +301,7 @@ let generate_principle  on_error
   let funs_types =  List.map (function ((_,_,_,types,_),_) -> types) fix_rec_l in
   try
     (* We then register the Inductive graphs of the functions  *)
-    Glob_term_to_relation.build_inductive names funs_args funs_types recdefs;
+    Glob_term_to_relation.build_inductive mp_dp names funs_args funs_types recdefs;
     if do_built
     then
       begin
@@ -549,7 +549,7 @@ let recompute_binder_list (fixpoint_exprl : (Vernacexpr.fixpoint_expr * Vernacex
   fixpoint_exprl_with_new_bl
   
 
-let do_generate_principle on_error register_built interactive_proof
+let do_generate_principle mp_dp on_error register_built interactive_proof
     (fixpoint_exprl:(Vernacexpr.fixpoint_expr * Vernacexpr.decl_notation list) list) :unit =
   List.iter (fun (_,l) -> if not (List.is_empty l) then error "Function does not support notations for now") fixpoint_exprl;
   let _is_struct =
@@ -566,6 +566,7 @@ let do_generate_principle on_error register_built interactive_proof
 	  let using_lemmas = [] in 
 	  let pre_hook =
 	    generate_principle
+	      mp_dp
 	      on_error
 	      true
 	      register_built
@@ -588,6 +589,7 @@ let do_generate_principle on_error register_built interactive_proof
 	  let body = match body with | Some body -> body | None -> user_err_loc (Loc.ghost,"Function",str "Body of Function must be given") in 
 	  let pre_hook =
 	    generate_principle
+	      mp_dp
 	      on_error
 	      true
 	      register_built
@@ -616,6 +618,7 @@ let do_generate_principle on_error register_built interactive_proof
 	let is_rec = List.exists (is_rec fix_names) recdefs in
 	if register_built then register_struct is_rec fixpoint_exprl;
 	generate_principle
+	  mp_dp
 	  on_error
 	  false
 	  register_built
@@ -803,17 +806,17 @@ let make_graph (f_ref:global_reference) =
 		 in
 		 l
 	     | _ ->
-		 let id = Label.to_id (con_label c) in
+		let id = Label.to_id (con_label c) in
 		 [((Loc.ghost,id),(None,Constrexpr.CStructRec),nal_tas,t,Some b),[]]
 	 in
-	 do_generate_principle error_error false false expr_list;
-	 (* We register the infos *)
 	 let mp,dp,_ = repr_con c in
+	 do_generate_principle (Some (mp,dp)) error_error  false false expr_list;
+	 (* We register the infos *)
 	 List.iter
 	   (fun (((_,id),_,_,_,_),_) -> add_Function false (make_con mp dp (Label.of_id id)))
 	   expr_list);
   Dumpglob.continue ()
 
-let do_generate_principle = do_generate_principle warning_error true
+let do_generate_principle = do_generate_principle None warning_error true