Evar_kinds.mli containing former Evd.hole_kind, avoid deps on Evd

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

5 files changed, 46 insertions, 43 deletions

diff --git a/toplevel/classes.ml b/toplevel/classes.ml
index dbabf6160..b3b9efcef 100644
--- a/toplevel/classes.ml
+++ b/toplevel/classes.ml
@@ -231,7 +231,7 @@ let new_instance ?(abstract=false) ?(global=false) ctx (instid, bk, cl) props
 			   k.cl_projs;
 			 c :: props, rest'
 		     with Not_found ->
-		       (CHole (Pp.dummy_loc, Some Evd.GoalEvar) :: props), rest
+		       (CHole (Pp.dummy_loc, Some Evar_kinds.GoalEvar) :: props), rest
 		   else props, rest)
 		([], props) k.cl_props
 	    in
diff --git a/toplevel/command.ml b/toplevel/command.ml
index 5aef9ec66..9e21a3a76 100644
--- a/toplevel/command.ml
+++ b/toplevel/command.ml
@@ -683,7 +683,7 @@ let build_wellfounded (recname,n,bl,arityc,body) r measure notation =
     mkApp (constr_of_global (delayed_force fix_sub_ref),
 	  [| argtyp ; wf_rel ;
 	     Evarutil.e_new_evar isevars env 
-	       ~src:(dummy_loc, Evd.QuestionMark (Evd.Define false)) wf_proof;
+	       ~src:(dummy_loc, Evar_kinds.QuestionMark (Evar_kinds.Define false)) wf_proof;
 	     prop ; intern_body_lam |])
   in
   let _ = isevars := Evarutil.nf_evar_map !isevars in
@@ -866,8 +866,8 @@ let check_program_evars env initial_sigma evd c =
 	  if not (Evd.mem initial_sigma evk) then
             let (loc,k) = Evd.evar_source evk evd in
 	      (match k with
-	      | Evd.QuestionMark _
-	      | Evd.ImplicitArg (_, _, false) -> ()
+	      | Evar_kinds.QuestionMark _
+	      | Evar_kinds.ImplicitArg (_, _, false) -> ()
 	      | _ ->
 		  let evi = nf_evar_info sigma (Evd.find sigma evk) in
 		    Pretype_errors.error_unsolvable_implicit loc env sigma evi k None)
diff --git a/toplevel/himsg.ml b/toplevel/himsg.ml
index 051eb3062..e0923cda0 100644
--- a/toplevel/himsg.ml
+++ b/toplevel/himsg.ml
@@ -342,35 +342,35 @@ let pr_ne_context_of header footer env =
   then footer
   else pr_ne_context_of header env
 
-let explain_hole_kind env evi = function
-  | QuestionMark _ -> str "this placeholder"
-  | CasesType ->
+let explain_evar_kind env evi = function
+  | Evar_kinds.QuestionMark _ -> str "this placeholder"
+  | Evar_kinds.CasesType ->
       str "the type of this pattern-matching problem"
-  | BinderType (Name id) ->
+  | Evar_kinds.BinderType (Name id) ->
       str "the type of " ++ Nameops.pr_id id
-  | BinderType Anonymous ->
+  | Evar_kinds.BinderType Anonymous ->
       str "the type of this anonymous binder"
-  | ImplicitArg (c,(n,ido),b) ->
+  | Evar_kinds.ImplicitArg (c,(n,ido),b) ->
       let id = Option.get ido in
       str "the implicit parameter " ++
       pr_id id ++ spc () ++ str "of" ++
       spc () ++ Nametab.pr_global_env Idset.empty c
-  | InternalHole ->
+  | Evar_kinds.InternalHole ->
       str "an internal placeholder" ++
 	Option.cata (fun evi ->
 	  let env = Evd.evar_env evi in
 	    str " of type "  ++ pr_lconstr_env env evi.evar_concl ++
 	      pr_ne_context_of (str " in environment:"++ fnl ()) (mt ()) env)
 	(mt ()) evi
-  | TomatchTypeParameter (tyi,n) ->
+  | Evar_kinds.TomatchTypeParameter (tyi,n) ->
       str "the " ++ pr_nth n ++
       str " argument of the inductive type (" ++ pr_inductive env tyi ++
       str ") of this term"
-  | GoalEvar ->
+  | Evar_kinds.GoalEvar ->
       str "an existential variable"
-  | ImpossibleCase ->
+  | Evar_kinds.ImpossibleCase ->
       str "the type of an impossible pattern-matching clause"
-  | MatchingVar _ ->
+  | Evar_kinds.MatchingVar _ ->
       assert false
 
 let explain_not_clean env sigma ev t k =
@@ -378,7 +378,7 @@ let explain_not_clean env sigma ev t k =
   let env = make_all_name_different env in
   let id = Evd.string_of_existential ev in
   let var = pr_lconstr_env env t in
-  str "Tried to instantiate " ++ explain_hole_kind env None k ++
+  str "Tried to instantiate " ++ explain_evar_kind env None k ++
   str " (" ++ str id ++ str ")" ++ spc () ++
   str "with a term using variable " ++ var ++ spc () ++
   str "which is not in its scope."
@@ -398,7 +398,7 @@ let explain_typeclass_resolution env evi k =
   | None -> mt()
 
 let explain_unsolvable_implicit env evi k explain =
-  str "Cannot infer " ++ explain_hole_kind env (Some evi) k ++
+  str "Cannot infer " ++ explain_evar_kind env (Some evi) k ++
   explain_unsolvability explain ++ str "." ++
   explain_typeclass_resolution env evi k
 
@@ -693,7 +693,7 @@ let explain_no_instance env (_,id) l =
   str "applied to arguments" ++ spc () ++
     pr_sequence (pr_lconstr_env env) l
 
-let is_goal_evar evi = match evi.evar_source with (_, GoalEvar) -> true | _ -> false
+let is_goal_evar evi = match evi.evar_source with (_, Evar_kinds.GoalEvar) -> true | _ -> false
 
 let pr_constraints printenv env evm =
   let evm = Evd.undefined_evars (Evarutil.nf_evar_map_undefined evm) in
diff --git a/toplevel/obligations.ml b/toplevel/obligations.ml
index 589403882..c6bb2c10a 100644
--- a/toplevel/obligations.ml
+++ b/toplevel/obligations.ml
@@ -49,8 +49,8 @@ let check_evars env evm =
   (fun (key, evi) ->
    let (loc,k) = evar_source key evm in
      match k with
-     | QuestionMark _
-     | ImplicitArg (_,_,false) -> ()
+     | Evar_kinds.QuestionMark _
+     | Evar_kinds.ImplicitArg (_,_,false) -> ()
      | _ ->
        Pretype_errors.error_unsolvable_implicit loc env
          evm (Evarutil.nf_evar_info evm evi) k None)
@@ -59,9 +59,9 @@ let check_evars env evm =
 type oblinfo =
   { ev_name: int * identifier;
     ev_hyps: named_context;
-    ev_status: obligation_definition_status;
+    ev_status: Evar_kinds.obligation_definition_status;
     ev_chop: int option;
-    ev_src: hole_kind located;
+    ev_src: Evar_kinds.t located;
     ev_typ: types;
     ev_tac: tactic option;
     ev_deps: Intset.t }
@@ -252,13 +252,13 @@ let eterm_obligations env name evm fs ?status t ty =
 	   | None -> evtyp, hyps, 0
 	 in
 	 let loc, k = evar_source id evm in
-	 let status = match k with QuestionMark o -> Some o | _ -> status in
+	 let status = match k with Evar_kinds.QuestionMark o -> Some o | _ -> status in
 	 let status, chop = match status with
-	   | Some (Define true as stat) ->
-	       if chop <> fs then Define false, None
+	   | Some (Evar_kinds.Define true as stat) ->
+	       if chop <> fs then Evar_kinds.Define false, None
 	       else stat, Some chop
 	   | Some s -> s, None
-	   | None -> Define true, None
+	   | None -> Evar_kinds.Define true, None
 	 in
 	 let tac = match evar_tactic.get ev.evar_extra with
 	   | Some t ->
@@ -284,7 +284,8 @@ let eterm_obligations env name evm fs ?status t ty =
 	    ev_src = src; ev_typ = typ; ev_deps = deps; ev_tac = tac } = info
       in
       let status = match status with
-	| Define true when Idset.mem name transparent -> Define false
+	| Evar_kinds.Define true when Idset.mem name transparent ->
+	  Evar_kinds.Define false
 	| _ -> status
       in name, typ, src, status, deps, tac) evts
   in
@@ -312,15 +313,16 @@ let explain_no_obligations = function
     Some ident -> str "No obligations for program " ++ str (string_of_id ident)
   | None -> str "No obligations remaining"
 
-type obligation_info = (Names.identifier * Term.types * hole_kind located *
-			  obligation_definition_status * Intset.t * tactic option) array
+type obligation_info =
+    (Names.identifier * Term.types * Evar_kinds.t located *
+     Evar_kinds.obligation_definition_status * Intset.t * tactic option) array
 
 type obligation =
   { obl_name : identifier;
     obl_type : types;
-    obl_location : hole_kind located;
+    obl_location : Evar_kinds.t located;
     obl_body : constr option;
-    obl_status : obligation_definition_status;
+    obl_status : Evar_kinds.obligation_definition_status;
     obl_deps : Intset.t;
     obl_tac : tactic option;
   }
@@ -391,7 +393,7 @@ let evar_of_obligation o = make_evar (Global.named_context_val ()) o.obl_type
 
 let get_obligation_body expand obl =
   let c = Option.get obl.obl_body in
-    if expand && obl.obl_status = Expand then
+    if expand && obl.obl_status = Evar_kinds.Expand then
       match kind_of_term c with
       | Const c -> constant_value (Global.env ()) c
       | _ -> c
@@ -603,8 +605,8 @@ let declare_obligation prg obl body =
   let body = prg.prg_reduce body in
   let ty = prg.prg_reduce obl.obl_type in
   match obl.obl_status with
-  | Expand -> { obl with obl_body = Some body }
-  | Define opaque ->
+  | Evar_kinds.Expand -> { obl with obl_body = Some body }
+  | Evar_kinds.Define opaque ->
       let opaque = if get_proofs_transparency () then false else opaque in
       let ce = 
 	{ const_entry_body = body;
@@ -628,8 +630,9 @@ let init_prog_info n b t deps fixkind notations obls impls kind reduce hook =
 	assert(obls = [||]);
 	let n = Nameops.add_suffix n "_obligation" in
 	  [| { obl_name = n; obl_body = None;
-	       obl_location = dummy_loc, InternalHole; obl_type = t;
-	       obl_status = Expand; obl_deps = Intset.empty; obl_tac = None } |],
+	       obl_location = dummy_loc, Evar_kinds.InternalHole; obl_type = t;
+	       obl_status = Evar_kinds.Expand; obl_deps = Intset.empty;
+	       obl_tac = None } |],
 	mkVar n
     | Some b ->
 	Array.mapi
@@ -726,7 +729,7 @@ let goal_fix_kind = Decl_kinds.Global, Decl_kinds.DefinitionBody Decl_kinds.Fixp
 
 let kind_of_opacity o =
   match o with
-  | Define false | Expand -> goal_kind
+  | Evar_kinds.Define false | Evar_kinds.Expand -> goal_kind
   | _ -> goal_proof_kind
 
 let not_transp_msg =
@@ -774,10 +777,10 @@ let rec solve_obligation prg num tac =
 		  let transparent = evaluable_constant cst (Global.env ()) in
 		  let body =
 		    match obl.obl_status with
-		    | Expand ->
+		    | Evar_kinds.Expand ->
 			if not transparent then error_not_transp ()
 			else constant_value (Global.env ()) cst
-		    | Define opaque ->
+		    | Evar_kinds.Define opaque ->
 			if not opaque && not transparent then error_not_transp ()
 			else Libnames.constr_of_global gr
 		  in
diff --git a/toplevel/obligations.mli b/toplevel/obligations.mli
index 16c00ce8f..df093ea43 100644
--- a/toplevel/obligations.mli
+++ b/toplevel/obligations.mli
@@ -39,8 +39,8 @@ val sort_dependencies : (int * evar_info * Intset.t) list -> (int * evar_info *
 (* env, id, evars, number of function prototypes to try to clear from
    evars contexts, object and type *)
 val eterm_obligations : env -> identifier -> evar_map -> int ->
-  ?status:obligation_definition_status -> constr -> types -> 
-  (identifier * types * hole_kind located * obligation_definition_status * Intset.t * 
+  ?status:Evar_kinds.obligation_definition_status -> constr -> types ->
+  (identifier * types * Evar_kinds.t located * Evar_kinds.obligation_definition_status * Intset.t *
       tactic option) array
     (* Existential key, obl. name, type as product, 
        location of the original evar, associated tactic,
@@ -52,8 +52,8 @@ val eterm_obligations : env -> identifier -> evar_map -> int ->
        translation from obligation identifiers to constrs, new term, new type *)
 
 type obligation_info =
-  (identifier * Term.types * hole_kind located *
-      obligation_definition_status * Intset.t * tactic option) array
+  (identifier * Term.types * Evar_kinds.t located *
+      Evar_kinds.obligation_definition_status * Intset.t * tactic option) array
     (* ident, type, location, (opaque or transparent, expand or define),
        dependencies, tactic to solve it *)