Improved tracking of the origin of evars.

5 files changed, 16 insertions, 11 deletions

diff --git a/intf/evar_kinds.mli b/intf/evar_kinds.mli
index e8281e07bb..f77fc5a6ab 100644
--- a/intf/evar_kinds.mli
+++ b/intf/evar_kinds.mli
@@ -28,3 +28,4 @@ type t =
   | ImpossibleCase
   | MatchingVar of bool * Id.t
   | VarInstance of Id.t
+  | SubEvar of t
diff --git a/pretyping/cases.ml b/pretyping/cases.ml
index 7da59b94e2..0005f83919 100644
--- a/pretyping/cases.ml
+++ b/pretyping/cases.ml
@@ -292,9 +292,9 @@ let try_find_ind env sigma typ realnames =
       | None -> List.make (List.length realargs) Anonymous in
   IsInd (typ,ind,names)
 
-let inh_coerce_to_ind evdref env ty tyi =
+let inh_coerce_to_ind evdref env loc ty tyi =
   let sigma = !evdref in
-  let expected_typ = inductive_template evdref env None tyi in
+  let expected_typ = inductive_template evdref env loc tyi in
   (* Try to refine the type with inductive information coming from the
      constructor and renounce if not able to give more information *)
   (* devrait être indifférent d'exiger leq ou pas puisque pour
@@ -320,7 +320,7 @@ let unify_tomatch_with_patterns evdref env loc typ pats realnames =
   match find_row_ind pats with
     | None -> NotInd (None,typ)
     | Some (_,(ind,_)) ->
-	inh_coerce_to_ind evdref env typ ind;
+	inh_coerce_to_ind evdref env loc typ ind;
 	try try_find_ind env !evdref typ realnames
 	with Not_found -> NotInd (None,typ)
 
diff --git a/pretyping/evarsolve.ml b/pretyping/evarsolve.ml
index 8694e8bbbd..2a819a018b 100644
--- a/pretyping/evarsolve.ml
+++ b/pretyping/evarsolve.ml
@@ -521,8 +521,8 @@ let make_projectable_subst aliases sigma evi args =
  * declares x1:T1..xq:Tq |- ?e : s such that ?e[u1..uq] = t holds.
  *)
 
-let define_evar_from_virtual_equation define_fun env evd t_in_env ty_t_in_sign sign filter inst_in_env =
-  let evd,evar_in_env = new_evar_instance sign evd ty_t_in_sign ~filter inst_in_env in
+let define_evar_from_virtual_equation define_fun env evd src t_in_env ty_t_in_sign sign filter inst_in_env =
+  let evd,evar_in_env = new_evar_instance sign evd ty_t_in_sign ~filter ~src inst_in_env in
   let t_in_env = whd_evar evd t_in_env in
   let evd = define_fun env evd None (destEvar evar_in_env) t_in_env in
   let ctxt = named_context_of_val sign in
@@ -552,6 +552,7 @@ let materialize_evar define_fun env evd k (evk1,args1) ty_in_env =
   let env1,rel_sign = env_rel_context_chop k env in
   let sign1 = evar_hyps evi1 in
   let filter1 = evar_filter evi1 in
+  let src = let (loc,k) = evi1.evar_source in (loc,Evar_kinds.SubEvar k) in
   let ids1 = List.map pi1 (named_context_of_val sign1) in
   let inst_in_sign = List.map mkVar (Filter.filter_list filter1 ids1) in
   let (sign2,filter2,inst2_in_env,inst2_in_sign,_,evd,_) =
@@ -560,12 +561,12 @@ let materialize_evar define_fun env evd k (evk1,args1) ty_in_env =
       let evd,t_in_sign =
         let s = Retyping.get_sort_of env evd t_in_env in
         let evd,ty_t_in_sign = refresh_universes ~inferred:true (Some false) env evd (mkSort s) in
-        define_evar_from_virtual_equation define_fun env evd t_in_env 
+        define_evar_from_virtual_equation define_fun env evd src t_in_env
           ty_t_in_sign sign filter inst_in_env in
       let evd,b_in_sign = match b with
       | None -> evd,None
       | Some b ->
-          let evd,b = define_evar_from_virtual_equation define_fun env evd b
+          let evd,b = define_evar_from_virtual_equation define_fun env evd src b
             t_in_sign sign filter inst_in_env in
           evd,Some b in
       (push_named_context_val (id,b_in_sign,t_in_sign) sign, Filter.extend 1 filter,
@@ -578,10 +579,10 @@ let materialize_evar define_fun env evd k (evk1,args1) ty_in_env =
   let evd,ev2ty_in_sign =
     let s = Retyping.get_sort_of env evd ty_in_env in
     let evd,ty_t_in_sign = refresh_universes ~inferred:true (Some false) env evd (mkSort s) in
-    define_evar_from_virtual_equation define_fun env evd ty_in_env
+    define_evar_from_virtual_equation define_fun env evd src ty_in_env
       ty_t_in_sign sign2 filter2 inst2_in_env in
   let evd,ev2_in_sign =
-    new_evar_instance sign2 evd ev2ty_in_sign ~filter:filter2 inst2_in_sign in
+    new_evar_instance sign2 evd ev2ty_in_sign ~filter:filter2 ~src inst2_in_sign in
   let ev2_in_env = (fst (destEvar ev2_in_sign), Array.of_list inst2_in_env) in
   (evd, ev2_in_sign, ev2_in_env)
 
diff --git a/pretyping/evd.ml b/pretyping/evd.ml
index 1d05d6c6e5..c9435b54c9 100644
--- a/pretyping/evd.ml
+++ b/pretyping/evd.ml
@@ -1599,7 +1599,7 @@ let pr_decl ((id,b,_),ok) =
   | Some c -> str (if ok then "(" else "{") ++ pr_id id ++ str ":=" ++
       print_constr c ++ str (if ok then ")" else "}")
 
-let pr_evar_source = function
+let rec pr_evar_source = function
   | Evar_kinds.QuestionMark _ -> str "underscore"
   | Evar_kinds.CasesType -> str "pattern-matching return predicate"
   | Evar_kinds.BinderType (Name id) -> str "type of " ++ Nameops.pr_id id
@@ -1615,6 +1615,7 @@ let pr_evar_source = function
   | Evar_kinds.ImpossibleCase -> str "type of impossible pattern-matching clause"
   | Evar_kinds.MatchingVar _ -> str "matching variable"
   | Evar_kinds.VarInstance id -> str "instance of " ++ pr_id id
+  | Evar_kinds.SubEvar k -> str "subterm of " ++ pr_evar_source k
 
 let pr_evar_info evi =
   let phyps =
diff --git a/toplevel/himsg.ml b/toplevel/himsg.ml
index 180ab3e8b4..3c52a6a314 100644
--- a/toplevel/himsg.ml
+++ b/toplevel/himsg.ml
@@ -501,7 +501,7 @@ let pr_trailing_ne_context_of env sigma =
   then str "."
   else (str " in environment:"++ fnl () ++ pr_context_unlimited env sigma)
 
-let explain_evar_kind env = function
+let rec explain_evar_kind env = function
   | Evar_kinds.QuestionMark _ -> strbrk "this placeholder"
   | Evar_kinds.CasesType ->
       strbrk "the type of this pattern-matching problem"
@@ -527,6 +527,8 @@ let explain_evar_kind env = function
       assert false
   | Evar_kinds.VarInstance id ->
       strbrk "an instance for the variable " ++ pr_id id
+  | Evar_kinds.SubEvar c ->
+      strbrk "a subterm of " ++ explain_evar_kind env c
 
 let explain_typeclass_resolution env sigma evi k =
   match Typeclasses.class_of_constr evi.evar_concl with