deplacement de clenv vers pretyping

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

7 files changed, 6 insertions, 675 deletions

diff --git a/proofs/clenv.ml b/proofs/clenv.ml
deleted file mode 100644
index a327a09f8..000000000
--- a/proofs/clenv.ml
+++ /dev/null
@@ -1,562 +0,0 @@
-(************************************************************************)
-(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
-(*   \VV/  **************************************************************)
-(*    //   *      This file is distributed under the terms of the       *)
-(*         *       GNU Lesser General Public License Version 2.1        *)
-(************************************************************************)
-
-(* $Id$ *)
-
-open Pp
-open Util
-open Names
-open Nameops
-open Term
-open Termops
-open Sign
-open Environ
-open Evd
-open Proof_type
-open Refiner
-open Proof_trees
-open Logic
-open Reductionops
-open Tacmach
-open Evar_refiner
-open Rawterm
-open Pattern
-open Tacexpr
-
-(* Generator of metavariables *)
-let new_meta =
-  let meta_ctr = ref 0 in
-  fun () -> incr meta_ctr; !meta_ctr
-
-(* replaces a mapping of existentials into a mapping of metas.
-   Problem if an evar appears in the type of another one (pops anomaly) *)
-let exist_to_meta sigma (emap, c) =
-  let metamap = ref [] in
-  let change_exist evar =
-    let ty = nf_betaiota (nf_evar emap (existential_type emap evar)) in
-    let n = new_meta() in
-    metamap := (n, ty) :: !metamap;
-    mkMeta n in
-  let rec replace c =
-    match kind_of_term c with
-        Evar (k,_ as ev) when not (Evd.in_dom sigma k) -> change_exist ev
-      | _ -> map_constr replace c in
-  (!metamap, replace c)
-
-(* collects all metavar occurences, in left-to-right order, preserving
- * repetitions and all. *)
-
-let collect_metas c = 
-  let rec collrec acc c =
-    match kind_of_term c with
-      | Meta mv -> mv::acc
-      | _         -> fold_constr collrec acc c
-  in
-  List.rev (collrec [] c)
-
-(* Clausal environments *)
-
-type 'a clausenv = {
-  templval : constr freelisted;
-  templtyp : constr freelisted;
-  namenv : identifier Metamap.t;
-  env : meta_map;
-  hook : 'a }
-
-type wc = named_context sigma
-
-
-(* [mentions clenv mv0 mv1] is true if mv1 is defined and mentions
- * mv0, or if one of the free vars on mv1's freelist mentions
- * mv0 *)
-
-let mentions clenv mv0 = 
-  let rec menrec mv1 =
-    try
-     (match Metamap.find mv1 clenv.env with
-	 | Clval (b,_) -> 
-	     Metaset.mem mv0 b.freemetas || meta_exists menrec b.freemetas
-	 | Cltyp _ -> false)
-    with Not_found -> 
-      false
-  in 
-  menrec
-
-(* Creates a new clause-environment, whose template has a given
- * type, CTY.  This is not all that useful, since not very often
- * does one know the type of the clause - one usually only has
- * a clause which one wants to backchain thru. *)
-
-let mk_clenv wc cty =
-  let mv = new_meta () in
-  let cty_fls = mk_freelisted cty in 
-  { templval = mk_freelisted (mkMeta mv);
-    templtyp = cty_fls;
-    namenv = Metamap.empty;
-    env =  Metamap.add mv (Cltyp cty_fls) Metamap.empty ;
-    hook = wc }
-  
-let clenv_environments bound c =
-  let rec clrec (ne,e,metas) n c =
-    match n, kind_of_term c with
-      | (Some 0, _) -> (ne, e, List.rev metas, c)
-      | (n, Cast (c,_)) -> clrec (ne,e,metas) n c
-      | (n, Prod (na,c1,c2)) ->
-	  let mv = new_meta () in
-	  let dep = dependent (mkRel 1) c2 in
-	  let ne' =
-	    if dep then
-              match na with
-		| Anonymous -> ne
-		| Name id ->
-		    if metamap_in_dom mv ne then begin
-		      warning ("Cannot put metavar "^(string_of_meta mv)^
-			       " in name-environment twice");
-		      ne
-		    end else 
-		      Metamap.add mv id ne
-            else 
-	      ne 
-	  in
-	  let e' = Metamap.add mv (Cltyp (mk_freelisted c1)) e in 
-	  clrec (ne',e', (mkMeta mv)::metas) (option_app ((+) (-1)) n)
-	    (if dep then (subst1 (mkMeta mv) c2) else c2)
-      | (n, LetIn (na,b,_,c)) ->
-	  clrec (ne,e,metas) (option_app ((+) (-1)) n) (subst1 b c)
-      | (n, _) -> (ne, e, List.rev metas, c)
-  in 
-  clrec (Metamap.empty,Metamap.empty,[]) bound c
-
-let mk_clenv_from_n wc n (c,cty) =
-  let (namenv,env,args,concl) = clenv_environments n cty in
-  { templval = mk_freelisted (match args with [] -> c | _ -> applist (c,args));
-    templtyp = mk_freelisted concl;
-    namenv = namenv;
-    env = env;
-    hook = wc }
-
-let mk_clenv_from wc = mk_clenv_from_n wc None
-
-let subst_clenv f sub clenv = 
-  { templval = map_fl (subst_mps sub) clenv.templval;
-    templtyp = map_fl (subst_mps sub) clenv.templtyp;
-    namenv = clenv.namenv;
-    env = Metamap.map (map_clb (subst_mps sub)) clenv.env;
-    hook = f sub clenv.hook }
-
-let connect_clenv gls clenv =
-  let wc = {it=gls.it.evar_hyps; sigma=gls.sigma} in
-  { clenv with hook = wc }
-
-let clenv_wtactic f clenv =
-  let (sigma',mmap') = f (clenv.hook.sigma, clenv.env) in
-  {clenv with env = mmap' ; hook = {it=clenv.hook.it; sigma=sigma'}}
-
-let mk_clenv_hnf_constr_type_of wc t =
-  mk_clenv_from wc (t,w_hnf_constr wc (w_type_of wc t))
-
-let mk_clenv_rename_from wc (c,t) = 
-  mk_clenv_from wc (c,rename_bound_var (w_env wc) [] t)
-
-let mk_clenv_rename_from_n wc n (c,t) = 
-  mk_clenv_from_n wc n (c,rename_bound_var (w_env wc) [] t)
-    
-let mk_clenv_rename_type_of wc t =
-  mk_clenv_from wc (t,rename_bound_var (w_env wc) [] (w_type_of wc t))
-    
-let mk_clenv_rename_hnf_constr_type_of wc t =
-  mk_clenv_from wc
-    (t,rename_bound_var (w_env wc) [] (w_hnf_constr wc (w_type_of wc t)))
-
-let mk_clenv_type_of wc t = mk_clenv_from wc (t,w_type_of wc t)
-			      
-let clenv_assign mv rhs clenv =
-  let rhs_fls = mk_freelisted rhs in 
-  if meta_exists (mentions clenv mv) rhs_fls.freemetas then
-    error "clenv__assign: circularity in unification";
-  try
-    (match Metamap.find mv clenv.env with
-       | Clval (fls,ty) ->
-	   if not (eq_constr fls.rebus rhs) then
-	     try 
-	       (* Streams are lazy, force evaluation of id to catch Not_found*)
-	       let id = Metamap.find mv clenv.namenv in
-	       errorlabstrm "clenv_assign"
-		 (str "An incompatible instantiation has already been found for " ++ 
-		    pr_id id)
-	     with Not_found ->
-	       anomaly "clenv_assign: non dependent metavar already assigned"
-	   else
-	     clenv
-       | Cltyp bty -> 
-	   { templval = clenv.templval;
-	     templtyp = clenv.templtyp;
-	     namenv = clenv.namenv;
-	     env = Metamap.add mv (Clval (rhs_fls,bty)) clenv.env;
-	     hook = clenv.hook })
-  with Not_found -> 
-    error "clenv_assign"
-
-let clenv_val_of clenv mv = 
-  let rec valrec mv =
-    try
-      (match Metamap.find mv clenv.env with
-	 | Cltyp _ -> mkMeta mv
-	 | Clval(b,_) ->
-	     instance (List.map (fun mv' -> (mv',valrec mv')) 
-			       (Metaset.elements b.freemetas)) b.rebus)
-    with Not_found -> 
-      mkMeta mv
-  in 
-  valrec mv
-
-let clenv_instance clenv b =
-  let c_sigma =
-    List.map 
-      (fun mv -> (mv,clenv_val_of clenv mv)) (Metaset.elements b.freemetas)
-  in 
-  instance c_sigma b.rebus
-    
-let clenv_instance_term clenv c =
-  clenv_instance clenv (mk_freelisted c)
-
-(* [clenv_pose (na,mv,cty) clenv]
- * returns a new clausenv which has added to it the metavar MV,
- * with type CTY.  the name NA, if it is not ANONYMOUS, will
- * be entered into the name-map, as a way of accessing the new
- * metavar. *)
-
-let clenv_pose (na,mv,cty) clenv =
-  { templval = clenv.templval;
-    templtyp = clenv.templtyp;
-    env = Metamap.add mv (Cltyp (mk_freelisted cty)) clenv.env;
-    namenv = (match na with
-		| Anonymous -> clenv.namenv
-		| Name id -> Metamap.add mv id clenv.namenv);
-    hook = clenv.hook }
-
-let clenv_defined clenv mv =
-  match Metamap.find mv clenv.env with
-    | Clval _ -> true
-    | Cltyp _ -> false
-
-let clenv_value clenv mv =
-  match Metamap.find mv clenv.env with
-    | Clval(b,_) -> b
-    | Cltyp _ -> failwith "clenv_value"
-	  
-let clenv_type clenv mv =
-  match Metamap.find mv clenv.env with
-    | Cltyp b -> b
-    | Clval(_,b) -> b
-	  
-let clenv_template clenv = clenv.templval
-
-let clenv_template_type clenv = clenv.templtyp
-
-let clenv_instance_value clenv mv =
-  clenv_instance clenv (clenv_value clenv mv)
-    
-let clenv_instance_type clenv mv =
-  clenv_instance clenv (clenv_type clenv mv)
-    
-let clenv_instance_template clenv =
-  clenv_instance clenv (clenv_template clenv)
-    
-let clenv_instance_template_type clenv =
-  clenv_instance clenv (clenv_template_type clenv)
-
-let clenv_type_of ce c =
-  let metamap =
-    List.map 
-      (function
-	 | (n,Clval(_,typ)) -> (n,typ.rebus)
-         | (n,Cltyp typ)    -> (n,typ.rebus))
-      (metamap_to_list ce.env)
-  in
-    Retyping.get_type_of_with_meta (w_env ce.hook) (w_Underlying ce.hook) metamap c
-
-let clenv_instance_type_of ce c =
-  clenv_instance ce (mk_freelisted (clenv_type_of ce c))
-
-let clenv_unify allow_K cv_pb t1 t2 clenv =
-  let env = w_env clenv.hook in
-  clenv_wtactic (Unification.w_unify allow_K env cv_pb t1 t2) clenv
-
-let clenv_unique_resolver allow_K clause gl =
-  clenv_unify allow_K CUMUL
-    (clenv_instance_template_type clause) (pf_concl gl) clause 
-
-(* [clenv_bchain mv clenv' clenv]
- *
- * Resolves the value of "mv" (which must be undefined) in clenv to be
- * the template of clenv' be the value "c", applied to "n" fresh
- * metavars, whose types are chosen by destructing "clf", which should
- * be a clausale forme generated from the type of "c".  The process of
- * resolution can cause unification of already-existing metavars, and
- * of the fresh ones which get created.  This operation is a composite
- * of operations which pose new metavars, perform unification on
- * terms, and make bindings.  *)
-
-let clenv_bchain mv subclenv clenv =
-  (* Add the metavars of [subclenv] to [clenv], with their name-environment *)
-  let clenv' =
-    { templval = clenv.templval;
-      templtyp = clenv.templtyp;
-      namenv =
-	List.fold_left (fun ne (mv,id) ->
-			  if clenv_defined subclenv mv then 
-			    ne
-			  else if metamap_in_dom mv ne then begin
-			    warning ("Cannot put metavar "^(string_of_meta mv)^
-				     " in name-environment twice");
-			    ne
-			  end else 
-			    Metamap.add mv id ne)
-          clenv.namenv (metamap_to_list subclenv.namenv);
-      env = List.fold_left (fun m (n,v) -> Metamap.add n v m) 
-	       clenv.env (metamap_to_list subclenv.env);
-      hook = clenv.hook } 
-  in
-  (* unify the type of the template of [subclenv] with the type of [mv] *)
-  let clenv'' =
-    clenv_unify true CUMUL
-      (clenv_instance clenv' (clenv_template_type subclenv))
-      (clenv_instance_type clenv' mv)
-      clenv' 
-  in
-  (* assign the metavar *)
-  let clenv''' =
-    clenv_assign mv (clenv_instance clenv' (clenv_template subclenv)) clenv''
-  in 
-  clenv'''
-
-
-(* swaps the "hooks" in [clenv1] and [clenv2], so we can then use
-   backchain to hook them together *)
-
-let clenv_swap clenv1 clenv2 =
-  let clenv1' = { templval = clenv1.templval;
-		  templtyp = clenv1.templtyp;
-		  namenv = clenv1.namenv;
-		  env = clenv1.env;
-		  hook = clenv2.hook} 
-  and clenv2' = { templval = clenv2.templval;
-		  templtyp = clenv2.templtyp;
-		  namenv = clenv2.namenv;
-		  env = clenv2.env;
-		  hook = clenv1.hook}
-  in 
-  (clenv1',clenv2')
-
-let clenv_fchain mv nextclenv clenv =
-  let (clenv',nextclenv') = clenv_swap clenv nextclenv in 
-  clenv_bchain mv clenv' nextclenv'
-
-(* [clenv_metavars clenv mv]
- * returns a list of the metavars which appear in the type of
- * the metavar mv.  The list is unordered. *)
-
-let clenv_metavars clenv mv =
-  match Metamap.find mv clenv.env with
-    | Clval(_,b) -> b.freemetas
-    | Cltyp b -> b.freemetas
-
-let clenv_template_metavars clenv = clenv.templval.freemetas
-
-(* [clenv_dependent hyps_only clenv]
- * returns a list of the metavars which appear in the template of clenv,
- * and which are dependent, This is computed by taking the metavars in cval,
- * in right-to-left order, and collecting the metavars which appear
- * in their types, and adding in all the metavars appearing in the
- * type of clenv.
- * If [hyps_only] then metavariables occurring in the type are _excluded_ *)
-
-let dependent_metas clenv mvs conclmetas =
-  List.fold_right
-    (fun mv deps ->
-       Metaset.union deps (clenv_metavars clenv mv))
-    mvs conclmetas
-
-let clenv_dependent hyps_only clenv =
-  let mvs = collect_metas (clenv_instance_template clenv) in
-  let ctyp_mvs = (mk_freelisted (clenv_instance_template_type clenv)).freemetas in
-  let deps = dependent_metas clenv mvs ctyp_mvs in
-  List.filter
-    (fun mv -> Metaset.mem mv deps && not (hyps_only && Metaset.mem mv ctyp_mvs))
-    mvs
-
-let clenv_missing c = clenv_dependent true c
-
-(* [clenv_independent clenv]
- * returns a list of metavariables which appear in the term cval,
- * and which are not dependent.  That is, they do not appear in
- * the types of other metavars which are in cval, nor in the type
- * of cval, ctyp. *)
-
-let clenv_independent clenv =
-  let mvs = collect_metas (clenv_instance_template clenv) in
-  let ctyp_mvs = (mk_freelisted (clenv_instance_template_type clenv)).freemetas in
-  let deps = dependent_metas clenv mvs ctyp_mvs in
-  List.filter (fun mv -> not (Metaset.mem mv deps)) mvs
-
-let w_coerce wc c ctyp target =
-  let j = make_judge c ctyp in
-  let env = w_env wc in
-  let isevars = Evarutil.create_evar_defs (w_Underlying wc) in
-  let j' = Coercion.inh_conv_coerce_to dummy_loc env isevars j target in
-  (* faire quelque chose avec isevars ? *)
-  j'.uj_val
-
-let clenv_constrain_dep_args hyps_only clause = function
-  | [] -> clause 
-  | mlist ->
-      let occlist = clenv_dependent hyps_only clause in
-      if List.length occlist = List.length mlist then
-	List.fold_left2
-          (fun clenv k c ->
-	    let wc = clause.hook in
-	    try
-	      let k_typ = w_hnf_constr wc (clenv_instance_type clause k) in
-	      let c_typ = w_hnf_constr wc (w_type_of wc c) in
-	      let c' = w_coerce wc c c_typ k_typ in
-	      clenv_unify true CONV (mkMeta k) c' clenv
-	    with _ ->
-              clenv_unify true CONV (mkMeta k) c clenv)
-          clause occlist mlist
-      else 
-	error ("Not the right number of missing arguments (expected "
-	       ^(string_of_int (List.length occlist))^")")
-
-let clenv_constrain_missing_args mlist clause =
-  clenv_constrain_dep_args true clause mlist
-
-let clenv_lookup_name clenv id =
-  match metamap_inv clenv.namenv id with
-    | []  -> 
-	errorlabstrm "clenv_lookup_name"
-          (str"No such bound variable " ++ pr_id id)
-    | [n] -> 
-	n
-    |  _  -> 
-	 anomaly "clenv_lookup_name: a name occurs more than once in clause"
-
-let clenv_match_args s clause =
-  let mvs = clenv_independent clause in 
-  let rec matchrec clause = function
-    | [] -> clause
-    | (loc,b,c)::t ->
-	let k =
-	  match b with
-            | NamedHyp s ->
-		if List.exists (fun (_,b',_) -> b=b') t then 
-		  errorlabstrm "clenv_match_args" 
-		    (str "The variable " ++ pr_id s ++ 
-		    str " occurs more than once in binding")
-		else
-		  clenv_lookup_name clause s
-	    | AnonHyp n ->
-		if List.exists (fun (_,b',_) -> b=b') t then
-		  errorlabstrm "clenv_match_args"
-		    (str "The position " ++ int n ++
-		    str " occurs more than once in binding");
-		try 
-		  List.nth mvs (n-1)
-		with (Failure _|Invalid_argument _) ->
-                  errorlabstrm "clenv_match_args" (str "No such binder")
-	in
-	let k_typ = w_hnf_constr clause.hook (clenv_instance_type clause k)
-	(* nf_betaiota was before in type_of - useful to reduce types like *)
-	(* (x:A)([x]P u) *)
-	and c_typ = w_hnf_constr clause.hook
-          (nf_betaiota (w_type_of clause.hook c)) in
-	let cl =
-	  (* Try to infer some Meta/Evar from the type of [c] *)
-	  try 
-            clenv_assign k c (clenv_unify true CUMUL c_typ k_typ clause)
-	  with _ ->
-	  (* Try to coerce to the type of [k]; cannot merge with the
-	     previous case because Coercion does not handle Meta *)
-          let c' = w_coerce clause.hook c c_typ k_typ in
-	  try clenv_unify true CONV (mkMeta k) c' clause
-	  with Pretype_errors.PretypeError
-              (_,Pretype_errors.CannotUnify (m,n)) ->
-	    Stdpp.raise_with_loc loc
- 	      (RefinerError (CannotUnifyBindingType (m,n)))
-	in matchrec cl t
-  in 
-  matchrec clause s
-
-type arg_bindings = (int * constr) list
-
-let clenv_constrain_with_bindings bl clause =
-  if bl = [] then 
-    clause 
-  else 
-    let all_mvs = collect_metas (clenv_template clause).rebus in
-    let rec matchrec clause = function
-      | []       -> clause
-      | (n,c)::t ->
-          let k = 
-            (try
-              if n > 0 then 
-		List.nth all_mvs (n-1)
-              else if n < 0 then 
-		List.nth (List.rev all_mvs) (-n-1)
-              else error "clenv_constrain_with_bindings" 
-            with Failure _ ->
-              errorlabstrm "clenv_constrain_with_bindings"
-                (str"Clause did not have " ++ int n ++ str"-th" ++
-                str" absolute argument")) in
-	  let env = Global.env () in
-	  let sigma = Evd.empty in
-	  let k_typ = nf_betaiota (clenv_instance_type clause k) in
-	  let c_typ = nf_betaiota (w_type_of clause.hook c) in 
-	  matchrec
-            (clenv_assign k c (clenv_unify true CUMUL c_typ k_typ clause)) t
-    in 
-    matchrec clause bl
-
-
-(***************************)
-
-(* Clausal environment for an application *)
-
-let make_clenv_binding_gen n wc (c,t) = function
-  | ImplicitBindings largs ->
-      let clause = mk_clenv_from_n wc n (c,t) in
-      clenv_constrain_dep_args (n <> None) clause largs
-  | ExplicitBindings lbind ->
-      let clause = mk_clenv_rename_from_n wc n (c,t) in
-      clenv_match_args lbind clause
-  | NoBindings ->
-      mk_clenv_from_n wc n (c,t)
-
-let make_clenv_binding_apply wc n = make_clenv_binding_gen (Some n) wc
-let make_clenv_binding = make_clenv_binding_gen None
-
-open Printer
-
-let pr_clenv clenv =
-  let pr_name mv =
-    try 
-      let id = Metamap.find mv clenv.namenv in
-      (str"[" ++ pr_id id ++ str"]")
-    with Not_found -> (mt ())
-  in
-  let pr_meta_binding = function
-    | (mv,Cltyp b) ->
-      	hov 0 
-	  (pr_meta mv ++ pr_name mv ++ str " : " ++ prterm b.rebus ++ fnl ())
-    | (mv,Clval(b,_)) ->
-      	hov 0 
-	  (pr_meta mv ++ pr_name mv ++ str " := " ++ prterm b.rebus ++ fnl ())
-  in
-  (str"TEMPL: " ++ prterm clenv.templval.rebus ++
-     str" : " ++ prterm clenv.templtyp.rebus ++ fnl () ++
-     (prlist pr_meta_binding (metamap_to_list clenv.env)))
diff --git a/proofs/clenv.mli b/proofs/clenv.mli
deleted file mode 100644
index 5ca846b06..000000000
--- a/proofs/clenv.mli
+++ /dev/null
@@ -1,104 +0,0 @@
-(************************************************************************)
-(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
-(*   \VV/  **************************************************************)
-(*    //   *      This file is distributed under the terms of the       *)
-(*         *       GNU Lesser General Public License Version 2.1        *)
-(************************************************************************)
-
-(*i $Id$ i*)
-
-(*i*)
-open Util
-open Names
-open Term
-open Sign
-open Evd
-open Proof_type
-(*i*)
-
-(* [new_meta] is a generator of unique meta variables *)
-val new_meta : unit -> metavariable
-
-(* [exist_to_meta] generates new metavariables for each existential
-   and performs the replacement in the given constr *)
-val exist_to_meta :
-  Evd.evar_map -> Pretyping.open_constr -> (Termops.metamap * constr)
-
-(* The Type of Constructions clausale environments. *)
-
-type 'a clausenv = {
-  templval : constr freelisted;
-  templtyp : constr freelisted;
-  namenv : identifier Metamap.t;
-  env : meta_map;
-  hook : 'a }
-
-type wc = named_context sigma (* for a better reading of the following *)
-
-(* [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. *)
-
-val collect_metas : constr -> metavariable list
-val mk_clenv : 'a -> constr -> 'a clausenv
-val mk_clenv_from : 'a -> constr * constr -> 'a clausenv
-val mk_clenv_from_n : 'a -> int option -> constr * constr -> 'a clausenv
-val mk_clenv_rename_from : wc -> constr * constr -> wc clausenv
-val mk_clenv_rename_from_n : wc -> int option -> constr * constr -> wc clausenv
-val mk_clenv_hnf_constr_type_of : wc -> constr -> wc clausenv
-val mk_clenv_type_of : wc -> constr -> wc clausenv
-
-val subst_clenv : (substitution -> 'a -> 'a) -> 
-  substitution -> 'a clausenv -> 'a clausenv
-val clenv_wtactic :
-  (evar_map * meta_map -> evar_map * meta_map) -> wc clausenv -> wc clausenv
-
-val connect_clenv : goal sigma -> 'a clausenv -> wc clausenv
-val clenv_assign : metavariable -> constr -> 'a clausenv -> 'a clausenv
-val clenv_instance_term : wc clausenv -> constr -> constr
-val clenv_pose : name * metavariable * constr -> 'a clausenv -> 'a clausenv
-val clenv_template : 'a clausenv -> constr freelisted
-val clenv_template_type : 'a clausenv -> constr freelisted
-val clenv_instance_type : wc clausenv -> metavariable -> constr
-val clenv_instance_template : wc clausenv -> constr
-val clenv_instance_template_type : wc clausenv -> constr
-val clenv_instance : 'a clausenv -> constr freelisted -> constr
-val clenv_type_of : wc clausenv -> constr -> constr
-val clenv_fchain : metavariable -> 'a clausenv -> wc clausenv -> wc clausenv
-val clenv_bchain : metavariable -> 'a clausenv -> wc clausenv -> wc clausenv
-
-(* Unification with clenv *)
-type arg_bindings = (int * constr) list
-
-val clenv_unify : 
-  bool -> Reductionops.conv_pb -> constr -> constr ->
-  wc clausenv -> wc clausenv
-val clenv_match_args :
-  constr Rawterm.explicit_bindings -> wc clausenv -> wc clausenv
-val clenv_constrain_with_bindings : arg_bindings -> wc clausenv -> wc clausenv
-
-(* Bindings *)
-val clenv_independent : wc clausenv -> metavariable list
-val clenv_dependent : bool -> 'a clausenv -> metavariable list
-val clenv_missing : 'a clausenv -> metavariable list
-val clenv_constrain_missing_args : (* Used in user contrib Lannion *)
-  constr list -> wc clausenv -> wc clausenv
-(*
-val clenv_constrain_dep_args : constr list -> wc clausenv -> wc clausenv
-*)
-val clenv_lookup_name : 'a clausenv -> identifier -> metavariable
-val clenv_unique_resolver : bool -> wc clausenv -> goal sigma -> wc clausenv
-
-val make_clenv_binding_apply :
-  wc -> int -> constr * constr -> types Rawterm.bindings -> wc clausenv
-val make_clenv_binding :
-  wc -> constr * constr -> types Rawterm.bindings -> wc clausenv
-
-(* Pretty-print *)
-val pr_clenv : 'a clausenv -> Pp.std_ppcmds
diff --git a/proofs/logic.ml b/proofs/logic.ml
index 314e3c597..82994669b 100644
--- a/proofs/logic.ml
+++ b/proofs/logic.ml
@@ -25,7 +25,6 @@ open Proof_trees
 open Proof_type
 open Typeops
 open Type_errors
-open Coqast
 open Retyping
 open Evarutil
  
@@ -40,7 +39,6 @@ type refiner_error =
   | NonLinearProof of constr
 
   (* Errors raised by the tactics *)
-  | CannotUnifyBindingType of constr * constr
   | IntroNeedsProduct
   | DoesNotOccurIn of constr * identifier
 
@@ -51,8 +49,10 @@ open Pretype_errors
 let catchable_exception = function
   | Util.UserError _ | TypeError _ | RefinerError _
   (* unification errors *)
-  | PretypeError(_,(CannotUnify _|CannotGeneralize _|NoOccurrenceFound _))
-  | Stdpp.Exc_located(_,PretypeError(_,(CannotUnify _|CannotGeneralize _|NoOccurrenceFound _)))
+  | PretypeError(_,(CannotUnify _|CannotGeneralize _|NoOccurrenceFound _|
+      CannotUnifyBindingType _))
+  | Stdpp.Exc_located(_,PretypeError(_,(CannotUnify _|CannotGeneralize _|
+          NoOccurrenceFound _ | CannotUnifyBindingType _)))
   | Stdpp.Exc_located(_,(Util.UserError _ | TypeError _ | RefinerError _ |
     Nametab.GlobalizationError _ | PretypeError (_,VarNotFound _))) -> true
   | _ -> false
diff --git a/proofs/logic.mli b/proofs/logic.mli
index 34e5b9e98..0a641e975 100644
--- a/proofs/logic.mli
+++ b/proofs/logic.mli
@@ -54,7 +54,6 @@ type refiner_error =
   | NonLinearProof of constr
 
   (*i Errors raised by the tactics i*)
-  | CannotUnifyBindingType of constr * constr
   | IntroNeedsProduct
   | DoesNotOccurIn of constr * identifier
 
diff --git a/proofs/refiner.ml b/proofs/refiner.ml
index 248f6b40b..a0053d8a1 100644
--- a/proofs/refiner.ml
+++ b/proofs/refiner.ml
@@ -21,7 +21,6 @@ open Type_errors
 open Proof_trees
 open Proof_type
 open Logic
-open Printer
 
 type transformation_tactic = proof_tree -> (goal list * validation)
 
@@ -952,7 +951,7 @@ let rec print_proof sigma osign pf =
 )
 	  
 let pr_change gl = 
-  (str"Change " ++ prterm_env (Global.env()) gl.evar_concl ++ str".")
+  (str"Change " ++ Printer.prterm_env (Global.env()) gl.evar_concl ++ str".")
 
 let rec print_script nochange sigma osign pf =
   let {evar_hyps=sign; evar_concl=cl} = pf.goal in
@@ -969,6 +968,7 @@ let rec print_script nochange sigma osign pf =
            prlist_with_sep pr_fnl
              (print_script nochange sigma sign) spfl)
 
+(* printed by Show Script command *)
 let print_treescript nochange sigma _osign pf =
   let rec aux top pf =
     let {evar_hyps=sign; evar_concl=cl} = pf.goal in
diff --git a/proofs/tacmach.ml b/proofs/tacmach.ml
index 1b1e88e82..0ea076edd 100644
--- a/proofs/tacmach.ml
+++ b/proofs/tacmach.ml
@@ -238,7 +238,6 @@ let rename_hyp id id'  = with_check (rename_hyp_no_check id id')
 (* Pretty-printers *)
 
 open Pp
-open Printer
 open Tacexpr
 open Rawterm
 
diff --git a/proofs/tactic_debug.ml b/proofs/tactic_debug.ml
index 1fa1101d6..cfa65119f 100644
--- a/proofs/tactic_debug.ml
+++ b/proofs/tactic_debug.ml
@@ -6,7 +6,6 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-open Ast
 open Names
 open Constrextern
 open Pp