module Wcclausenv

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

4 files changed, 25 insertions, 22 deletions

diff --git a/proofs/clenv.ml b/proofs/clenv.ml
index 5ec52db76d..21fc10bf73 100644
--- a/proofs/clenv.ml
+++ b/proofs/clenv.ml
@@ -882,8 +882,11 @@ let clenv_type_of ce c =
          | (n,Cltyp typ)    -> (n,typ.rebus))
       (intmap_to_list ce.env)
   in
+  failwith "TODO: clenv_type_of"
+  (***
   (Trad.ise_resolve true (w_Underlying ce.hook) metamap
      (gLOB(w_hyps ce.hook)) c)._TYPE
+  ***)
 
 let clenv_instance_type_of ce c =
   clenv_instance ce (mk_freelisted (clenv_type_of ce c))
@@ -959,7 +962,8 @@ let clenv_typed_fo_resolver clenv gls =
 
 let args_typ gls = 
   let rec decrec l c = match pf_whd_betadeltaiota gls c with
-    | DOP2(Prod,a,DLAM(n,b)) -> decrec ((Environ.named_hd a n,a)::l) b
+    | DOP2(Prod,a,DLAM(n,b)) -> 
+	decrec ((Environ.named_hd Environ.empty_env a n,a)::l) b
     | x -> l
   in 
   decrec []
@@ -984,9 +988,7 @@ let abstract_list_all gls typ c l =
     if pf_conv_x gls (pf_type_of gls p) typ then p else 
       error "abstract_list_all"
   with UserError _ ->
-    let pt = pTERMINENV (gLOB (pf_hyps gls), typ) in
-    errorlabstrm "abstract_list_all"
-      [< 'sTR "cannot find a generalisation of the goal with type : "; pt >]
+    raise (RefinerError (CannotGeneralize (pf_hyps gls,typ)))
 
 let secondOrderAbstraction allow_K gl p oplist clause =
   let (clause',cllist) = 
diff --git a/proofs/clenv.mli b/proofs/clenv.mli
index b5675f1a12..de56125af5 100644
--- a/proofs/clenv.mli
+++ b/proofs/clenv.mli
@@ -26,17 +26,16 @@ type 'a clausenv = {
   env : clbinding Intmap.t;
   hook : 'a }
 
-(* templval is the template which we are trying to fill out.
- * templtyp is its type.
- * namenv is a mapping from metavar numbers to names, for
- *        use in instanciating metavars by name.
- * env is the mapping from metavar numbers to their types
- *     and values.
- * hook is the pointer to the current walking context, for
- *      integrating existential vars and metavars.
- *)
+(* [templval] is the template which we are trying to fill out.
+ * [templtyp] is its type.
+ * [namenv] is a mapping from metavar numbers to names, for
+ *          use in instanciating metavars by name.
+ * [env] is the mapping from metavar numbers to their types
+ *       and values.
+ * [hook] is the pointer to the current walking context, for
+ *        integrating existential vars and metavars. *)
 
-type wc = walking_constraints (* Pour une meilleure lisibilité *)
+type wc = walking_constraints (* for a better reading of the following *)
 
 val unify : constr -> tactic
 val unify_0 : 
@@ -54,13 +53,13 @@ val mk_clenv_type_of : wc -> constr -> wc clausenv
 val connect_clenv : wc -> 'a clausenv -> wc clausenv
 val clenv_change_head : constr * constr -> 'a clausenv -> 'a clausenv
 val clenv_assign : int -> constr -> 'a clausenv -> 'a clausenv
-val clenv_instance_term : 'a clausenv -> constr -> constr
+val clenv_instance_term : wc clausenv -> constr -> constr
 val clenv_pose : name * int * constr -> 'a clausenv -> 'a clausenv
 val clenv_template : 'a clausenv -> constr freelisted
 val clenv_template_type : 'a clausenv -> constr freelisted
-val clenv_instance_type : 'a clausenv -> int -> constr
-val clenv_instance_template : 'a clausenv -> constr
-val clenv_instance_template_type : 'a clausenv -> constr
+val clenv_instance_type : wc clausenv -> int -> constr
+val clenv_instance_template : wc clausenv -> constr
+val clenv_instance_template_type : wc clausenv -> constr
 val clenv_unify : constr -> constr -> wc clausenv -> wc clausenv
 val clenv_fchain : int -> 'a clausenv -> wc clausenv -> wc clausenv
 val clenv_refine : (wc -> tactic) -> wc clausenv -> tactic
@@ -68,9 +67,9 @@ val res_pf      : (wc -> tactic) -> wc clausenv -> tactic
 val res_pf_cast : (wc -> tactic) -> wc clausenv -> tactic
 val elim_res_pf : (wc -> tactic) -> wc clausenv -> tactic
 val clenv_independent : 
-  'a clausenv -> constr freelisted * constr freelisted -> int list
+  wc clausenv -> constr freelisted * constr freelisted -> int list
 val clenv_missing : 
-  'a clausenv -> constr freelisted * constr freelisted -> int list
+  wc clausenv -> constr freelisted * constr freelisted -> int list
 val clenv_constrain_missing_args : constr list -> wc clausenv -> wc clausenv
 val clenv_constrain_dep_args : constr list -> wc clausenv -> wc clausenv
 val clenv_lookup_name : 'a clausenv -> identifier -> int
diff --git a/proofs/logic.ml b/proofs/logic.ml
index e619c70b00..b0823c1b2d 100644
--- a/proofs/logic.ml
+++ b/proofs/logic.ml
@@ -21,6 +21,8 @@ type refiner_error =
   | OccurMeta of constr
   | CannotApply of constr * constr
   | CannotUnify of constr * constr
+  | CannotGeneralize of typed_type signature * constr
+  | NotWellTyped of constr
   | BadTacticArgs of string * tactic_arg list
 
 exception RefinerError of refiner_error
diff --git a/proofs/logic.mli b/proofs/logic.mli
index d8c71f7605..59f9cdf69f 100644
--- a/proofs/logic.mli
+++ b/proofs/logic.mli
@@ -28,8 +28,8 @@ type refiner_error =
   | OccurMeta of constr
   | CannotApply of constr * constr
   | CannotUnify of constr * constr
+  | CannotGeneralize of typed_type signature * constr
+  | NotWellTyped of constr
   | BadTacticArgs of string * tactic_arg list
 
-exception RefinerError of refiner_error
-
 val error_cannot_unify : path_kind -> constr * constr -> 'a