Fix bug #1913, checking for unresolved evars which aren't obligations.

Also check mutuality of fixpoints.


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

3 files changed, 32 insertions, 18 deletions

diff --git a/contrib/subtac/subtac_command.ml b/contrib/subtac/subtac_command.ml
index 5bff6ad1a..a2f54b02d 100644
--- a/contrib/subtac/subtac_command.ml
+++ b/contrib/subtac/subtac_command.ml
@@ -350,9 +350,27 @@ let compute_possible_guardness_evidences (n,_) (_, fixctx) fixtype =
 
 let push_named_context = List.fold_right push_named
 
+let check_evars env initial_sigma evd c =
+  let sigma = evars_of evd in
+  let c = nf_evar sigma c in
+  let rec proc_rec c =
+    match kind_of_term c with
+      | Evar (evk,args) ->
+          assert (Evd.mem sigma evk);
+	  if not (Evd.mem initial_sigma evk) then
+            let (loc,k) = evar_source evk evd in
+	      (match k with
+	      | QuestionMark _ -> ()
+	      | _ ->
+		  let evi = nf_evar_info sigma (Evd.find sigma evk) in
+		    Pretype_errors.error_unsolvable_implicit loc env sigma evi k None)
+      | _ -> iter_constr proc_rec c
+  in proc_rec c
+
 let interp_recursive fixkind l boxed =
   let env = Global.env() in
   let fixl, ntnl = List.split l in
+  let kind = if fixkind <> Command.IsCoFixpoint then Fixpoint else CoFixpoint in
   let fixnames = List.map (fun fix -> fix.Command.fix_name) fixl in
 
   (* Interp arities allowing for unresolved types *)
@@ -384,20 +402,17 @@ let interp_recursive fixkind l boxed =
   let rec_sign = nf_named_context_evar (evars_of evd) rec_sign in
     
   let recdefs = List.length rec_sign in
-(*   List.iter (check_evars env_rec Evd.empty evd) fixdefs; *)
-(*   List.iter (check_evars env Evd.empty evd) fixtypes; *)
-(*   check_mutuality env kind (List.combine fixnames fixdefs); *)
+  List.iter (check_evars env_rec Evd.empty evd) fixdefs;
+  List.iter (check_evars env Evd.empty evd) fixtypes;
+  Command.check_mutuality env kind (List.combine fixnames fixdefs);
 
   (* Russell-specific code *)
 
   (* Get the interesting evars, those that were not instanciated *)
   let isevars = Evd.undefined_evars evd in
-  trace (str "got undefined evars" ++ Evd.pr_evar_defs isevars);
   let evm = Evd.evars_of isevars in
-  trace (str "got the evm, recdefs is " ++ int recdefs);
   (* Solve remaining evars *)
   let rec collect_evars id def typ imps = 
-    let _ = try trace (str "In collect evars, isevars is: " ++ Evd.pr_evar_defs isevars) with _ -> () in
       (* Generalize by the recursive prototypes  *)
     let def = 
       Termops.it_mkNamedLambda_or_LetIn def rec_sign
diff --git a/contrib/subtac/subtac_command.mli b/contrib/subtac/subtac_command.mli
index 27520867f..3a6a351ba 100644
--- a/contrib/subtac/subtac_command.mli
+++ b/contrib/subtac/subtac_command.mli
@@ -42,6 +42,7 @@ val interp_binder :     Evd.evar_defs ref ->
     Environ.env -> Names.name -> Topconstr.constr_expr -> Term.constr
 
 
+
 val build_recursive :
   (fixpoint_expr * decl_notation) list -> bool -> unit
 
diff --git a/toplevel/command.mli b/toplevel/command.mli
index 595057616..227152f14 100644
--- a/toplevel/command.mli
+++ b/toplevel/command.mli
@@ -56,18 +56,16 @@ val declare_assumption : identifier located list ->
 val declare_interning_data : 'a * Constrintern.implicits_env ->
     string * Topconstr.constr_expr * Topconstr.scope_name option -> unit
 
-
-val compute_interning_datas :  Environ.env ->
-    'a list ->
-    'b list ->
-    Term.types list ->
-    Impargs.manual_explicitation list list ->
+val compute_interning_datas :  Environ.env -> 'a list -> 'b list ->
+  Term.types list ->Impargs.manual_explicitation list list ->
   'a list *
-    ('b *
-	(Names.identifier list * Impargs.implicits_list *
-	    Topconstr.scope_name option list))
+    ('b * (Names.identifier list * Impargs.implicits_list *
+	      Topconstr.scope_name option list))
     list
 
+val check_mutuality : Environ.env -> definition_object_kind ->
+  (identifier * types) list -> unit
+
 val build_mutual : (inductive_expr * decl_notation) list -> bool -> unit
 
 val declare_mutual_with_eliminations :
@@ -87,10 +85,10 @@ type fixpoint_expr = {
   fix_type : constr_expr
 }
 
-val recursive_message : Decl_kinds.definition_object_kind ->
-  int array option -> Names.identifier list -> Pp.std_ppcmds
+val recursive_message : definition_object_kind ->
+  int array option -> identifier list -> Pp.std_ppcmds
   
-val declare_fix : bool -> Decl_kinds.definition_object_kind -> identifier ->
+val declare_fix : bool -> definition_object_kind -> identifier ->
   constr -> types -> Impargs.manual_explicitation list -> global_reference
 
 val build_recursive : (Topconstr.fixpoint_expr * decl_notation) list -> bool -> unit