Ajout d'un LetIn primitif.

Abstraction de constr via kind_of_constr dans une bonne partie du code.


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

9 files changed, 295 insertions, 334 deletions

diff --git a/proofs/clenv.ml b/proofs/clenv.ml
index 4c2cbf987..ab301c450 100644
--- a/proofs/clenv.ml
+++ b/proofs/clenv.ml
@@ -4,7 +4,7 @@
 open Pp
 open Util
 open Names
-open Generic
+(*i open Generic i*)
 open Term
 open Sign
 open Instantiate
@@ -35,30 +35,26 @@ type wc = walking_constraints
 let new_evar_in_sign env =
   let ids = ids_of_var_context (Environ.var_context env) in
   let ev = new_evar () in
-  DOPN(Evar ev, Array.of_list (List.map (fun id -> VAR id) ids))
+  mkEvar (ev, Array.of_list (List.map (fun id -> VAR id) ids))
 
-let rec whd_evar env sigma = function
-  | DOPN(Evar ev,_) as k ->
-      if is_defined sigma ev then
-        whd_evar env sigma (constant_value env k)
-      else 
-	collapse_appl k
-  | t -> 
-      collapse_appl t
+let rec whd_evar sigma t = match kind_of_term t with
+  | IsEvar (ev,_ as evc) when is_defined sigma ev ->
+      whd_evar sigma (existential_value sigma evc)
+  | _ -> collapse_appl t
 
 let applyHead n c wc = 
   let rec apprec n c cty wc =
     if n = 0 then 
       (wc,c)
     else 
-      match w_whd_betadeltaiota wc cty with
-        | DOP2(Prod,c1,DLAM(_,c2)) ->
+      match kind_of_term (w_whd_betadeltaiota wc cty) with
+        | IsProd (_,c1,c2) ->
             let c1ty = w_type_of wc c1 in
 	    let evar = new_evar_in_sign (w_env wc) in
             let (evar_n, _) = destEvar evar in
 	    (compose 
 	       (apprec (n-1) (applist(c,[evar])) (subst1 evar c2))
-	       (w_Declare evar_n (DOP2(Cast,c1,c1ty))))
+	       (w_Declare evar_n (c1,c1ty)))
 	    wc
 	| _ -> error "Apply_Head_Then"
   in 
@@ -82,77 +78,63 @@ let unify_0 mc wc m n =
   let env = w_env wc
   and sigma = w_Underlying wc in
   let rec unirec_rec ((metasubst,evarsubst) as substn) m n =
-    let cM = whd_evar env sigma m
-    and cN = whd_evar env sigma n in 
+    let cM = whd_evar sigma m
+    and cN = whd_evar sigma n in 
     try 
-      match (cM,cN) with
-	| DOP2(Cast,c,_),t2 -> unirec_rec substn c t2
-	| t1,DOP2(Cast,c,_) -> unirec_rec substn t1 c
-	| DOP0(Meta k),_    -> (k,cN)::metasubst,evarsubst
-	| cM,DOP0(Meta(k))    -> (k,cM)::metasubst,evarsubst
-	| DOP2(Lambda,t1,DLAM(_,c1)),DOP2(Lambda,t2,DLAM(_,c2)) ->
+      match (kind_of_term cM,kind_of_term cN) with
+	| IsCast (c,_), _ -> unirec_rec substn c cN
+	| _, IsCast (c,_) -> unirec_rec substn cM c
+	| IsMeta k, _    -> (k,cN)::metasubst,evarsubst
+	| _, IsMeta k    -> (k,cM)::metasubst,evarsubst
+	| IsLambda (_,t1,c1), IsLambda (_,t2,c2) ->
 	    unirec_rec (unirec_rec substn t1 t2) c1 c2
-	| DOP2(Prod,t1,DLAM(_,c1)),DOP2(Prod,t2,DLAM(_,c2)) ->
+	| IsProd (_,t1,c1), IsProd (_,t2,c2) ->
 	    unirec_rec (unirec_rec substn t1 t2) c1 c2
 
-	| DOPN(AppL,cl1),DOPN(AppL,cl2) ->
-	    let len1 = Array.length cl1
-	    and len2 = Array.length cl2 in
+	| IsAppL (f1,l1), IsAppL (f2,l2) ->
+	    let len1 = List.length l1
+	    and len2 = List.length l2 in
 	    if len1 = len2 then
-              array_fold_left2 unirec_rec substn cl1 cl2
+              List.fold_left2 unirec_rec (unirec_rec substn f1 f2) l1 l2
 	    else if len1 < len2 then
-              let extras,restcl2 = array_chop ((len2-len1)+1) cl2 in 
-	      array_fold_left2 unirec_rec 
-		(unirec_rec substn (array_hd cl1) (DOPN(AppL,extras)))
-                (array_tl cl1) restcl2
+              let extras,restl2 = list_chop (len2-len1) l2 in 
+	      List.fold_left2 unirec_rec 
+		(unirec_rec substn f1 (applist (f2,extras)))
+                l1 restl2
 	    else 
-	      let extras,restcl1 = array_chop ((len1-len2)+1) cl1 in 
-	      array_fold_left2 unirec_rec 
-		(unirec_rec substn (DOPN(AppL,extras)) (array_hd cl2))
-                restcl1 (array_tl cl2)
+	      let extras,restl1 = list_chop (len1-len2) l1 in 
+	      List.fold_left2 unirec_rec 
+		(unirec_rec substn (applist (f1,extras)) f2)
+                restl1 l2
 		
-	| DOPN(MutCase _,_),DOPN(MutCase _,_) ->
-	    let (_,p1,c1,cl1) = destCase cM 
-	    and (_,p2,c2,cl2) = destCase cN in
-	    if Array.length cl1 = Array.length cl2 then
-              array_fold_left2 unirec_rec 
-		(unirec_rec (unirec_rec substn p1 p2) c1 c2) cl1 cl2
-	    else 
-	      error_cannot_unify CCI (m,n)
+	| IsMutCase (_,p1,c1,cl1), IsMutCase (_,p2,c2,cl2) ->
+            array_fold_left2 unirec_rec 
+	      (unirec_rec (unirec_rec substn p1 p2) c1 c2) cl1 cl2
 		
-	| DOPN(MutConstruct _,_),DOPN(MutConstruct _,_) ->
+	| IsMutConstruct _, IsMutConstruct _ ->
 	    if is_conv env sigma cM cN then
 	      substn
 	    else
 	      error_cannot_unify CCI (m,n)
 	      
-	| DOPN(MutInd _,_),DOPN(MutInd _,_) ->
+	| IsMutInd _, IsMutInd _ ->
 	    if is_conv env sigma  cM cN then
 	      substn
 	    else
 	      error_cannot_unify CCI (m,n)
 	      
-	| (DOPN(Evar _,_)),(DOPN((Const _ | Evar _),_)) ->
+	| IsEvar _, _ ->
 	    metasubst,((cM,cN)::evarsubst)
-	| (DOPN((Const _ | Evar _),_)),(DOPN(Evar _,_)) ->
+	| _, IsEvar _ ->
 	    metasubst,((cN,cM)::evarsubst)
-	| (DOPN(Const _,_)),(DOPN(Const _,_)) ->
-	    if is_conv env sigma cM cN then 
-	      substn
-	    else 
-	      error_cannot_unify CCI (m,n)
-		
-	| (DOPN(Evar _,_)),_ ->
-	    metasubst,((cM,cN)::evarsubst)
-	| (DOPN(Const _,_)),_ ->
+
+	| IsConst _, _ ->
 	    if is_conv env sigma cM cN then
 	      substn
 	    else 
 	      error_cannot_unify CCI (m,n)
 		
-	| _,(DOPN(Evar _,_)) ->
-	    metasubst,((cN,cM)::evarsubst)
-	| _,(DOPN(Const _,_)) ->
+	| _, IsConst _ ->
 	    if (not (occur_meta cM)) & is_conv env sigma cM cN then 
 	      substn
 	    else 
@@ -173,19 +155,16 @@ let unify_0 mc wc m n =
       unirec_rec (mc,[]) m n
 
 	
-let whd_castappevar_stack sigma = 
-  let rec whrec x l =
-    match x with
-      | DOPN(Evar ev,args) as c ->
-	  if is_defined sigma ev then
-	    whrec (existential_value sigma (ev,args)) l
-	  else
-	    x,l
-      | DOP2(Cast,c,_) -> whrec c l
-      | DOPN(AppL,cl) -> whrec (array_hd cl) (array_app_tl cl l)
-      | x -> x,l
+let whd_castappevar_stack sigma c l = 
+  let rec whrec (c, l as s) =
+    match kind_of_term c with
+      | IsEvar (ev,args) when is_defined sigma ev -> 
+	  whrec (existential_value sigma (ev,args), l)
+      | IsCast (c,_) -> whrec (c, l)
+      | IsAppL (f,args) -> whrec (f, args@l)
+      | _ -> s
   in 
-  whrec
+  whrec (c,l)
 
 let whd_castappevar sigma c = applist(whd_castappevar_stack sigma c [])
 
@@ -247,27 +226,29 @@ let rec w_Unify m n mc wc =
 and w_resrec metas evars wc =
   match evars with
     | [] -> (wc,metas)
-	  
-    | (lhs,(DOP0(Meta k) as rhs))::t -> w_resrec ((k,lhs)::metas) t wc
-	  
-    | (DOPN(Evar evn,_) as evar,rhs)::t ->
-	if w_defined_evar wc evn then
-          let (wc',metas') = w_Unify rhs evar metas wc in 
-	  w_resrec metas' t wc'
-	else
-          (try 
-	     w_resrec metas t (w_Define evn rhs wc)
-           with ex when catchable_exception ex ->
-             (match rhs with
-             	| DOPN(AppL,cl) ->
-		    (match cl.(0) with
-		       | DOPN(Const sp,_) ->
-			   let wc' = mimick_evar cl.(0) 
-				       ((Array.length cl) - 1) evn wc in
-			   w_resrec metas evars wc'
-		       | _ -> error "w_Unify")
-		| _ -> error "w_Unify"))
-    | _ -> anomaly "w_resrec"
+
+    | (lhs,rhs) :: t ->
+    match kind_of_term rhs with
+
+      | IsMeta k -> w_resrec ((k,lhs)::metas) t wc
+
+      | krhs ->
+      match kind_of_term lhs with
+
+	| IsEvar (evn,_) ->
+	    if w_defined_evar wc evn then
+	      let (wc',metas') = w_Unify rhs lhs metas wc in 
+	      w_resrec metas' t wc'
+	    else
+	      (try 
+		 w_resrec metas t (w_Define evn rhs wc)
+               with ex when catchable_exception ex ->
+		 (match krhs with
+             	    | IsAppL (f,cl) when isConst f ->
+			let wc' = mimick_evar f (List.length cl) evn wc in
+			w_resrec metas evars wc'
+		    | _ -> error "w_Unify"))
+	| _ -> anomaly "w_resrec"
 
 
 (* [unifyTerms] et [unify] ne semble pas gérer les Meta, en
@@ -284,30 +265,20 @@ let unify m gls =
  * repetitions and all. *)
 
 let collect_metas c = 
-  let rec collrec c acc =
-    match c with
-      | DOP0(Meta mv)    -> mv::acc
-      | DOP1(oper,c)     -> collrec c acc
-      | DOP2(oper,c1,c2) -> collrec c1 (collrec c2 acc)
-      | DOPN(oper,cl)    -> Array.fold_right collrec cl acc
-      | DLAM(_,c)        -> collrec c acc
-      | DLAMV(_,v)       -> Array.fold_right collrec v acc
-      | _                -> acc
-  in 
-  collrec c []
+  let rec collrec acc c =
+    match splay_constr c with
+      | OpMeta mv, _ -> mv::acc
+      | _, cl        -> Array.fold_left collrec acc cl
+  in
+  List.rev (collrec [] c)
 
 let metavars_of c =  
-  let rec collrec c acc =
-    match c with
-      | DOP0(Meta mv)    -> Intset.add mv acc
-      | DOP1(oper,c)     -> collrec c acc
-      | DOP2(oper,c1,c2) -> collrec c1 (collrec c2 acc)
-      | DOPN(oper,cl)    -> Array.fold_right collrec cl acc
-      | DLAM(_,c)        -> collrec c acc
-      | DLAMV(_,v)       -> Array.fold_right collrec v acc
-      | _                -> acc
+  let rec collrec acc c =
+    match splay_constr c with
+      | OpMeta mv, _ -> Intset.add mv acc
+      | _, cl       ->  Array.fold_left collrec acc cl
   in 
-  collrec c Intset.empty
+  collrec Intset.empty c
 
 let mk_freelisted c =
   { rebus = c; freemetas = metavars_of c }
@@ -336,7 +307,7 @@ let mentions clenv mv0 =
 let mk_clenv wc cty =
   let mv = new_meta () in
   let cty_fls = mk_freelisted cty in 
-  { templval = mk_freelisted(DOP0(Meta mv));
+  { templval = mk_freelisted (mkMeta mv);
     templtyp = cty_fls;
     namenv = Intmap.empty;
     env =  Intmap.add mv (Cltyp cty_fls) Intmap.empty ;
@@ -344,12 +315,12 @@ let mk_clenv wc cty =
   
 let clenv_environments bound c =
   let rec clrec (ne,e,metas) n c =
-    match n,c with
-      | (0, hd) -> (ne,e,List.rev metas,hd)
-      | (n, (DOP2(Cast,c,_))) -> clrec (ne,e,metas) n c
-      | (n, (DOP2(Prod,c1,DLAM(na,c2)))) ->
+    match n, kind_of_term c with
+      | (0, _) -> (ne, e, List.rev metas, c)
+      | (n, IsCast (c,_)) -> clrec (ne,e,metas) n c
+      | (n, IsProd (na,c1,c2)) ->
 	  let mv = new_meta () in
-	  let dep = dependent (Rel 1) c2 in
+	  let dep = dependent (mkRel 1) c2 in
 	  let ne' =
 	    if dep then
               match na with
@@ -365,18 +336,15 @@ let clenv_environments bound c =
 	      ne 
 	  in
 	  let e' = Intmap.add mv (Cltyp (mk_freelisted c1)) e in 
-	  clrec (ne',e',DOP0(Meta mv)::metas) (n-1)
-	    (if dep then (subst1 (DOP0(Meta mv)) c2) else c2)
-      | (n, hd) -> (ne,e,List.rev metas,hd)
+	  clrec (ne',e', (mkMeta mv)::metas) (n-1)
+	    (if dep then (subst1 (mkMeta mv) c2) else c2)
+      | (n, _) -> (ne, e, List.rev metas, c)
   in 
   clrec (Intmap.empty,Intmap.empty,[]) bound c
 
 let mk_clenv_from wc (c,cty) =
   let (namenv,env,args,concl) = clenv_environments (-1) cty in
-  { templval = 
-      mk_freelisted (match args with 
-		       | [] -> c 
-		       | _ -> DOPN(AppL,Array.of_list (c::args)));
+  { templval = mk_freelisted (match args with [] -> c | _ -> applist (c,args));
     templtyp = mk_freelisted concl;
     namenv = namenv;
     env = env;
@@ -433,12 +401,12 @@ let clenv_val_of clenv mv =
   let rec valrec mv =
     try
       (match Intmap.find mv clenv.env with
-	 | Cltyp _ -> DOP0(Meta mv)
+	 | Cltyp _ -> mkMeta mv
 	 | Clval(b,_) ->
 	     instance (List.map (fun mv' -> (mv',valrec mv')) 
 			       (Intset.elements b.freemetas)) b.rebus)
     with Not_found -> 
-      DOP0(Meta mv)
+      mkMeta mv
   in 
   valrec mv
 
@@ -461,16 +429,10 @@ let clenv_instance_term clenv c =
 
 let clenv_cast_meta clenv = 
   let rec crec u =
-    match u with
-      | DOPN((AppL|MutCase _),_)  -> crec_hd u
-      | DOP2(Cast,DOP0(Meta _),_) -> u
-      | DOPN(c,cl)                -> DOPN(c,Array.map crec cl)
-      | DOPL(c,cl)                -> DOPL(c,List.map crec cl)
-      | DOP1(c,t)                 -> DOP1(c,crec t)
-      | DOP2(c,t1,t2)             -> DOP2(c,crec t1,crec t2)
-      | DLAM(n,c)                 -> DLAM(n,crec c)
-      | DLAMV(n,cl)               -> DLAMV(n,Array.map crec cl)
-      | x                         -> x
+    match splay_constr u with
+      | (OpAppL | OpMutCase _), _ -> crec_hd u
+      | OpCast , [|c;_|] when isMeta c -> u
+      | op, cl  -> gather_constr (op, Array.map crec cl)
 	    
   and crec_hd u =
     match kind_of_term (strip_outer_cast u) with
@@ -479,7 +441,7 @@ let clenv_cast_meta clenv =
 	     match Intmap.find mv clenv.env with
                | Cltyp b ->
 		   let b' = clenv_instance clenv b in 
-		   if occur_meta b' then u else mkCast u b'
+		   if occur_meta b' then u else mkCast (u, b')
 	       | Clval(_) -> u
 	   with Not_found -> 
 	     u)
@@ -569,30 +531,35 @@ let clenv_instance_type_of ce c =
 let clenv_merge with_types =
   let rec clenv_resrec metas evars clenv =
     match (evars,metas) with
-      | ([],[]) -> clenv
-
-      | ((lhs,(DOP0(Meta k) as rhs))::t,metas) ->
-    	  clenv_resrec ((k,lhs)::metas) t clenv
-
-      | ((DOPN(Evar evn,_) as evar,rhs)::t,metas) ->
-    	  if w_defined_const clenv.hook evar then
-            let (metas',evars') = unify_0 [] clenv.hook rhs evar in
-            clenv_resrec (metas'@metas) (evars'@t) clenv
-    	  else
-            (try 
-	       clenv_resrec metas t (clenv_wtactic (w_Define evn rhs) clenv)
-             with ex when catchable_exception ex ->
-               (match rhs with
-		  | DOPN(AppL,cl) ->
-		      (match cl.(0) with
-			 | (DOPN(Const _,_) | DOPN(MutConstruct _,_)) ->
-			     clenv_resrec metas evars 
-			       (clenv_wtactic (mimick_evar cl.(0) 
-						 ((Array.length cl) - 1) evn) 
-				  clenv)
-			 | _ -> error "w_Unify")
-           	  | _ -> error "w_Unify"))
-      | ([],(mv,n)::t) ->
+      | ([], []) -> clenv
+
+      | ((lhs,rhs)::t, metas) ->
+      (match kind_of_term rhs with
+
+	| IsMeta k -> clenv_resrec ((k,lhs)::metas) t clenv
+
+	| krhs ->
+        (match kind_of_term lhs with
+
+	  | IsEvar (evn,_) ->
+    	      if w_defined_evar clenv.hook evn then
+		let (metas',evars') = unify_0 [] clenv.hook rhs lhs in
+		clenv_resrec (metas'@metas) (evars'@t) clenv
+    	      else
+		(try 
+		   clenv_resrec metas t
+		     (clenv_wtactic (w_Define evn rhs) clenv)
+		 with ex when catchable_exception ex ->
+		   (match krhs with
+		      | IsAppL (f,cl) when isConst f or isMutConstruct f ->
+			  clenv_resrec metas evars 
+			    (clenv_wtactic (mimick_evar f (List.length cl) evn)
+			       clenv)
+           	      | _ -> error "w_Unify"))
+
+	  | _ -> anomaly "clenv_resrec"))
+
+      | ([], (mv,n)::t) ->
     	  if clenv_defined clenv mv then
             let (metas',evars') =
               unify_0 [] clenv.hook (clenv_value clenv mv).rebus n in
@@ -606,8 +573,6 @@ let clenv_merge with_types =
 	      else ([],[]) in
 	    clenv_resrec (mc@t) ec (clenv_assign mv n clenv)
 
-      | _ -> anomaly "clenv_resrec"
-
   in clenv_resrec
 
 (* [clenv_unify M N clenv]
@@ -707,39 +672,34 @@ let clenv_refine_cast kONT clenv gls =
    try to find a subterm of cl which matches op, if op is just a Meta
    FAIL because we cannot find a binding *)
 
-let constrain_clenv_to_subterm clause = function 
-  | (DOP0(Meta(_)) as op),_ -> error "Match_subterm"
-  | op,cl -> 
-      let rec matchrec cl =
-    	let cl = strip_outer_cast cl in
-    	(try 
-	   if closed0 cl 
-	   then clenv_unify op cl clause,cl
-           else error "Bound 1"
-	 with ex when catchable_exception ex ->
-           (match telescope_appl cl with 
-	      | DOPN(AppL,tl) ->
-		  if Array.length tl = 2 then
-               	    let c1 = tl.(0) and c2 = tl.(1) in
-		    (try 
-		       matchrec c1 
-		     with ex when catchable_exception ex -> 
-		       matchrec c2)
-		  else 
-		    error "Match_subterm"
-              | DOP2(Prod,t,DLAM(_,c)) ->
-		  (try 
-		     matchrec t 
-		   with ex when catchable_exception ex -> 
-		     matchrec c)
-              | DOP2(Lambda,t,DLAM(_,c)) ->
-		  (try 
-		     matchrec t 
-		   with ex when catchable_exception ex -> 
-		     matchrec c)
-              | _ -> error "Match_subterm")) 
-      in 
-      matchrec cl
+let constrain_clenv_to_subterm clause (op,cl) =
+  let rec matchrec cl =
+    let cl = strip_outer_cast cl in
+    (try 
+       if closed0 cl 
+       then clenv_unify op cl clause,cl
+       else error "Bound 1"
+     with ex when catchable_exception ex ->
+       (match kind_of_term (telescope_appl cl) with 
+	  | IsAppL (c1,[c2]) ->
+	      (try 
+		 matchrec c1 
+	       with ex when catchable_exception ex -> 
+		 matchrec c2)
+          | IsProd (_,t,c) ->
+	      (try 
+		 matchrec t 
+	       with ex when catchable_exception ex -> 
+		 matchrec c)
+          | IsLambda (_,t,c) ->
+	      (try 
+		 matchrec t 
+	       with ex when catchable_exception ex -> 
+		 matchrec c)
+          | _ -> error "Match_subterm")) 
+  in 
+  if isMeta op then error "Match_subterm";
+  matchrec cl
 
 (* Possibly gives K-terms in case the operator does not contain 
    a meta : BUG ?? *)
@@ -822,7 +782,7 @@ let clenv_constrain_missing_args mlist clause =
     let occlist = clenv_missing clause (clenv_template clause,
                                    	(clenv_template_type clause)) in 
     if List.length occlist = List.length mlist then
-      List.fold_left2 (fun clenv occ m -> clenv_unify (DOP0(Meta occ)) m clenv)
+      List.fold_left2 (fun clenv occ m -> clenv_unify (mkMeta occ) m clenv)
         clause occlist mlist
     else 
       error ("Not the right number of missing arguments (expected "
@@ -835,7 +795,7 @@ let clenv_constrain_dep_args mlist clause =
     let occlist = clenv_dependent clause (clenv_template clause,
 					  (clenv_template_type clause)) in 
     if List.length occlist = List.length mlist then
-      List.fold_left2 (fun clenv occ m -> clenv_unify (DOP0(Meta occ)) m clenv)
+      List.fold_left2 (fun clenv occ m -> clenv_unify (mkMeta occ) m clenv)
         clause occlist mlist
     else 
       error ("Not the right number of missing arguments (expected "
@@ -848,7 +808,7 @@ let clenv_constrain_dep_args_of mv mlist clause =
     let occlist = clenv_dependent clause (clenv_value clause mv,
                                           clenv_type clause mv) in 
     if List.length occlist = List.length mlist then
-      List.fold_left2 (fun clenv occ m -> clenv_unify (DOP0(Meta occ)) m clenv)
+      List.fold_left2 (fun clenv occ m -> clenv_unify (mkMeta occ) m clenv)
         clause occlist mlist
     else 
       error ("clenv_constrain_dep_args_of: Not the right number " ^ 
@@ -913,7 +873,7 @@ let clenv_pose_dependent_evars clenv =
        let (evar_n,_) = destEvar evar in
        let tY = clenv_instance_type clenv mv in
        let tYty = w_type_of clenv.hook tY in
-       let clenv' = clenv_wtactic (w_Declare evar_n (DOP2(Cast,tY,tYty))) 
+       let clenv' = clenv_wtactic (w_Declare evar_n (tY,tYty))
 		      clenv in
        clenv_assign mv evar clenv')
     clenv
@@ -968,13 +928,14 @@ let secondOrderAbstraction allow_K gl p oplist clause =
   let (clause',cllist) = 
     constrain_clenv_using_subterm_list allow_K clause oplist (pf_concl gl) in
   let typp = clenv_instance_type clause' p in 
-  clenv_unify (DOP0(Meta p))
+  clenv_unify (mkMeta p)
     (abstract_list_all (pf_env gl) (project gl) typp (pf_concl gl) cllist) 
     clause'
 
 let clenv_so_resolver allow_K clause gl =
-  match whd_castapp_stack (clenv_instance_template_type clause) [] with
-    | (DOP0(Meta(p)),oplist) ->
+  let c, oplist = whd_castapp_stack (clenv_instance_template_type clause) [] in
+  match kind_of_term c with
+    | IsMeta p ->
 	let clause' = secondOrderAbstraction allow_K gl p oplist clause in 
 	clenv_fo_resolver clause' gl
     | _ -> error "clenv_so_resolver"
@@ -991,9 +952,10 @@ let clenv_so_resolver allow_K clause gl =
    Meta(1) had meta-variables in it. *)
 
 let clenv_unique_resolver allow_K clenv gls =
-  match (whd_castapp_stack (clenv_instance_template_type clenv) [],
-         whd_castapp_stack (pf_concl gls) []) with
-    | ((DOP0(Meta _) as pathd,_),(DOP2(Lambda,_,_) as glhd,_)) ->
+  let pathd,_ = whd_castapp_stack (clenv_instance_template_type clenv) [] in
+  let glhd,_ = whd_castapp_stack (pf_concl gls) [] in
+  match kind_of_term pathd, kind_of_term glhd with
+    | IsMeta _, IsLambda _ ->
 	(try 
 	   clenv_typed_fo_resolver clenv gls
 	 with ex when catchable_exception ex -> 
@@ -1002,7 +964,7 @@ let clenv_unique_resolver allow_K clenv gls =
 	   with ex when catchable_exception ex -> 
 	     error "Cannot solve a second-order unification problem")
 
-    | ((DOP0(Meta _),_),_) -> 
+    | IsMeta _, _ -> 
 	(try 
 	   clenv_so_resolver allow_K clenv gls
          with ex when catchable_exception ex -> 
diff --git a/proofs/evar_refiner.ml b/proofs/evar_refiner.ml
index abfe2305d..5cb4689ae 100644
--- a/proofs/evar_refiner.ml
+++ b/proofs/evar_refiner.ml
@@ -5,7 +5,7 @@ open Pp
 open Util
 open Stamps
 open Names
-open Generic
+(*i open Generic i*)
 open Term
 open Environ
 open Evd
@@ -120,11 +120,8 @@ let w_hyps    wc    = var_context (get_env (ids_it wc))
 let w_ORELSE wt1 wt2 wc = 
   try wt1 wc with e when catchable_exception e -> wt2 wc
 
-let w_Declare sp c (wc : walking_constraints) =
-  begin match c with 
-    | DOP2(Cast,_,_) -> ()
-    | _ -> error "Cannot declare an un-casted evar"
-  end;
+let w_Declare sp (ty,s) (wc : walking_constraints) =
+  let c = mkCast (ty,s) in
   let _ = w_type_of wc c in
   let access  = get_focus (ids_it wc)
   and env = get_env (ids_it wc)in
@@ -134,20 +131,15 @@ let w_Declare sp c (wc : walking_constraints) =
 let w_Declare_At sp sp' c = w_Focusing sp (w_Declare sp' c)
 
 let evars_of sigma constr = 
-  let rec filtrec acc = function
-    | DOP0 oper        -> acc
-    | VAR _            -> acc
-    | DOP1(oper,c)     -> filtrec acc c
-    | DOP2(oper,c1,c2) -> filtrec (filtrec acc c1) c2
-    | DOPN(Evar ev,cl) ->
-	let newacc = (Array.fold_left filtrec acc cl) in
-	if Evd.in_dom (ts_it sigma).decls ev
-	then Intset.add ev newacc else newacc
-    | DOPN(oper,cl)    -> Array.fold_left filtrec acc cl
-    | DOPL(oper,cl)    -> List.fold_left filtrec acc cl
-    | DLAM(_,c)        -> filtrec acc c
-    | DLAMV(_,v)       -> Array.fold_left filtrec acc v
-    | _                -> acc
+  let rec filtrec acc c =
+    match splay_constr c with
+    | OpEvar ev, cl ->
+	if Evd.in_dom (ts_it sigma).decls ev then
+	  Intset.add ev (Array.fold_left filtrec acc cl)
+	else
+	  Array.fold_left filtrec acc cl
+    | _, cl ->
+	Array.fold_left filtrec acc cl
   in 
   filtrec Intset.empty constr
 
@@ -155,7 +147,7 @@ let w_Define sp c wc =
   let spdecl = Evd.map (w_Underlying wc) sp in
   let cty = 
     try 
-      ctxt_type_of (ids_it (w_Focus sp wc)) (DOP2(Cast,c,spdecl.evar_concl))
+      ctxt_type_of (ids_it (w_Focus sp wc)) (mkCast (c,spdecl.evar_concl))
     with Not_found -> 
       error "Instantiation contains unlegal variables"
   in 
diff --git a/proofs/evar_refiner.mli b/proofs/evar_refiner.mli
index ef72c9d35..70416a363 100644
--- a/proofs/evar_refiner.mli
+++ b/proofs/evar_refiner.mli
@@ -33,8 +33,8 @@ val walking         : w_tactic -> tactic
 val w_Focusing_THEN : 
   evar -> 'a result_w_tactic -> ('a -> w_tactic) -> w_tactic
 
-val w_Declare    : evar -> constr -> w_tactic
-val w_Declare_At : evar -> evar -> constr -> w_tactic
+val w_Declare    : evar -> constr * constr -> w_tactic
+val w_Declare_At : evar -> evar -> constr * constr -> w_tactic
 val w_Define     : evar -> constr -> w_tactic
 
 val w_Underlying : walking_constraints -> evar_declarations
diff --git a/proofs/logic.ml b/proofs/logic.ml
index 8c577f9bc..a92276cc8 100644
--- a/proofs/logic.ml
+++ b/proofs/logic.ml
@@ -5,7 +5,7 @@ open Pp
 open Util
 open Names
 open Evd
-open Generic
+(*i open Generic i*)
 open Term
 open Sign
 open Environ
@@ -56,27 +56,25 @@ let conv_leq_goal env sigma arg ty conclty =
 
 let rec mk_refgoals sigma goal goalacc conclty trm =
   let env = goal.evar_env in
-  match trm with
-    | DOP0(Meta mv) ->
+  match kind_of_term trm with
+    | IsMeta mv ->
 	if occur_meta conclty then
           error "Cannot refine to conclusions with meta-variables";
 	let ctxt = out_some goal.evar_info in 
 	(mk_goal ctxt env (nf_betaiota env sigma conclty))::goalacc, conclty
 
-    | DOP2(Cast,t,ty) ->
+    | IsCast (t,ty) ->
 	let _ = type_of env sigma ty in
 	conv_leq_goal env sigma trm ty conclty;
 	mk_refgoals sigma goal goalacc ty t
 
-    | DOPN(AppL,cl) ->
-	let (acc',hdty) = mk_hdgoals sigma goal goalacc (array_hd cl) in
-	let (acc'',conclty') = 
-	  mk_arggoals sigma goal acc' hdty (array_list_of_tl cl) in
+    | IsAppL (f,l) ->
+	let (acc',hdty) = mk_hdgoals sigma goal goalacc f in
+	let (acc'',conclty') = mk_arggoals sigma goal acc' hdty l in
 	let _ = conv_leq_goal env sigma trm conclty' conclty in
         (acc'',conclty')
 
-    | DOPN(MutCase _,_) as mc -> 
-	let (_,p,c,lf) = destCase mc in
+    | IsMutCase (_,p,c,lf) ->
 	let (acc',lbrty,conclty') = mk_casegoals sigma goal goalacc p c in
 	let acc'' = 
 	  array_fold_left2
@@ -86,10 +84,10 @@ let rec mk_refgoals sigma goal goalacc conclty trm =
 	let _ = conv_leq_goal env sigma trm conclty' conclty in 
 	(acc'',conclty')
 
-    | t -> 
-	if occur_meta t then raise (RefinerError (OccurMeta t));
-      	let t'ty = type_of env sigma t in
-	conv_leq_goal env sigma t t'ty conclty;
+    | _ -> 
+	if occur_meta trm then raise (RefinerError (OccurMeta trm));
+      	let t'ty = type_of env sigma trm in
+	conv_leq_goal env sigma trm t'ty conclty;
         (goalacc,t'ty)
 
 (* Same as mkREFGOALS but without knowing te type of the term. Therefore,
@@ -97,18 +95,17 @@ let rec mk_refgoals sigma goal goalacc conclty trm =
 
 and mk_hdgoals sigma goal goalacc trm =
   let env = goal.evar_env in
-  match trm with
-    | DOP2(Cast,DOP0(Meta mv),ty) ->
+  match kind_of_term trm with
+    | IsCast (c,ty) when isMeta c ->
 	let _ = type_of env sigma ty in
 	let ctxt = out_some goal.evar_info in  
 	(mk_goal ctxt env (nf_betaiota env sigma ty))::goalacc,ty
-	  
-    | DOPN(AppL,cl) ->
-	let (acc',hdty) = mk_hdgoals sigma goal goalacc (array_hd cl) in
-	mk_arggoals sigma goal acc' hdty (array_list_of_tl cl)
-	
-    | DOPN(MutCase _,_) as mc -> 
-	let (_,p,c,lf) = destCase mc in
+
+    | IsAppL (f,l) ->
+	let (acc',hdty) = mk_hdgoals sigma goal goalacc f in
+	mk_arggoals sigma goal acc' hdty l
+
+    | IsMutCase (_,p,c,lf) ->
 	let (acc',lbrty,conclty') = mk_casegoals sigma goal goalacc p c in
 	let acc'' = 
 	  array_fold_left2
@@ -117,17 +114,19 @@ and mk_hdgoals sigma goal goalacc trm =
 	in
 	(acc'',conclty')
 
-    | t -> goalacc, type_of env sigma t
+    | _ -> goalacc, type_of env sigma trm
 
 and mk_arggoals sigma goal goalacc funty = function
   | [] -> goalacc,funty
-  | harg::tlargs ->
-      let env = goal.evar_env in
-      (match whd_betadeltaiota env sigma funty with
-	 | DOP2(Prod,c1,DLAM(_,b)) ->
-	     let (acc',hargty) = mk_refgoals sigma goal goalacc c1 harg in
-	     mk_arggoals sigma goal acc' (subst1 harg b) tlargs
-	 | t -> raise (RefinerError (CannotApply (t,harg))))
+  | harg::tlargs as allargs ->
+      let t = whd_betadeltaiota goal.evar_env sigma funty in
+      match kind_of_term t with
+	| IsProd (_,c1,b) ->
+	    let (acc',hargty) = mk_refgoals sigma goal goalacc c1 harg in
+	    mk_arggoals sigma goal acc' (subst1 harg b) tlargs
+	| IsLetIn (_,c1,_,b) ->
+	    mk_arggoals sigma goal goalacc (subst1 c1 b) allargs
+	| _ -> raise (RefinerError (CannotApply (t,harg)))
 
 and mk_casegoals sigma goal goalacc p c =
   let env = goal.evar_env in
@@ -144,28 +143,24 @@ and mk_casegoals sigma goal goalacc p c =
 varaibles only in Application and Case *)
 
 let collect_meta_variables c = 
-  let rec collrec acc = function
-    | DOP0(Meta mv) -> mv::acc
-    | DOP2(Cast,c,_) -> collrec acc c
-    | DOPN(AppL,cl) -> Array.fold_left collrec acc cl
-    | DOPN(MutCase _,_) as mc -> 
-	let (_,p,c,lf) = destCase mc in
-	Array.fold_left collrec (collrec (collrec acc p) c) lf
+  let rec collrec acc c = match splay_constr c with
+    | OpMeta mv, _ -> mv::acc
+    | OpCast, [|c;_|] -> collrec acc c
+    | (OpAppL | OpMutCase _), cl -> Array.fold_left collrec acc cl
     | _ -> acc
   in 
   List.rev(collrec [] c)
 
 let new_meta_variables = 
-  let rec newrec = function
-    | DOP0(Meta _) -> DOP0(Meta (new_meta()))
-    | DOP2(Cast,c,t) -> DOP2(Cast, newrec c, t)
-    | DOPN(AppL,cl) -> DOPN(AppL, Array.map newrec cl)
-    | DOPN(MutCase _,_) as mc ->
-        let (ci,p,c,lf) = destCase mc in
-        mkMutCaseA ci (newrec p) (newrec c) (Array.map newrec lf)
-    | x -> x
+  let rec newrec x = match kind_of_term x with
+    | IsMeta _ -> mkMeta (new_meta())
+    | IsCast (c,t) -> mkCast (newrec c, t)
+    | IsAppL (f,cl) -> applist (newrec f, List.map newrec cl)
+    | IsMutCase (ci,p,c,lf) ->
+	mkMutCaseA ci (newrec p) (newrec c) (Array.map newrec lf)
+    | _ -> x
   in 
-  newrec
+ newrec
 
 let error_use_instantiate () =
   errorlabstrm "Logic.prim_refiner"
@@ -299,13 +294,20 @@ let prim_refiner r sigma goal =
     | { name = Intro; newids = [id] } ->
     	if !check && mem_var_context id sign then
 	  error "New variable is already declared";
-        (match strip_outer_cast cl with
-	   | DOP2(Prod,c1,DLAM(_,b)) ->
+        (match kind_of_term (strip_outer_cast cl) with
+	   | IsProd (_,c1,b) ->
 	       if occur_meta c1 then error_use_instantiate();
 	       let a = get_assumption_of env sigma c1
 	       and v = VAR id in
 	       let sg = mk_goal info (push_var_decl (id,a) env) (subst1 v b) in
 	       [sg]
+	   | IsLetIn (_,c1,t1,b) ->
+	       if occur_meta c1 or occur_meta t1 then error_use_instantiate();
+	       let a = get_assumption_of env sigma t1
+	       and v = VAR id in
+	       let sg =
+		 mk_goal info (push_var_def (id,c1,a) env) (subst1 v b) in
+	       [sg]
 	   | _ ->
 	       if !check then error "Introduction needs a product"
 	       else anomaly "Intro: expects a product")
@@ -313,27 +315,41 @@ let prim_refiner r sigma goal =
     | { name = Intro_after; newids = [id]; hypspecs = [whereid] } ->
     	if !check && mem_var_context id sign then
 	  error "New variable is already declared";
-        (match strip_outer_cast cl with
-	   | DOP2(Prod,c1,DLAM(_,b)) ->
+        (match kind_of_term (strip_outer_cast cl) with
+	   | IsProd (_,c1,b) ->
 	       if occur_meta c1 then error_use_instantiate();
 	       let a = get_assumption_of env sigma c1
 	       and v = VAR id in
 	       let env' = insert_after_hyp env whereid (id,None,a) in
 	       let sg = mk_goal info env' (subst1 v b) in 
 	       [sg]
+	   | IsLetIn (_,c1,t1,b) ->
+	       if occur_meta c1 or occur_meta t1 then error_use_instantiate();
+	       let a = get_assumption_of env sigma t1
+	       and v = VAR id in
+	       let env' = insert_after_hyp env whereid (id,Some c1,a) in
+	       let sg = mk_goal info env' (subst1 v b) in 
+	       [sg]
 	   | _ ->
 	       if !check then error "Introduction needs a product"
 	       else anomaly "Intro_after: expects a product")
 	
     | { name = Intro_replacing; newids = []; hypspecs = [id] } ->
-	(match strip_outer_cast cl with
-           | DOP2(Prod,c1,DLAM(_,b)) ->
+	(match kind_of_term (strip_outer_cast cl) with
+           | IsProd (_,c1,b) ->
 	       if occur_meta c1 then error_use_instantiate();
 	       let a = get_assumption_of env sigma c1
 	       and v = VAR id in
 	       let env' = replace_hyp env id (id,None,a) in
 	       let sg = mk_goal info env' (subst1 v b) in
 	       [sg]
+           | IsLetIn (_,c1,t1,b) ->
+	       if occur_meta c1 then error_use_instantiate();
+	       let a = get_assumption_of env sigma t1
+	       and v = VAR id in
+	       let env' = replace_hyp env id (id,Some c1,a) in
+	       let sg = mk_goal info env' (subst1 v b) in
+	       [sg]
 	   | _ ->
 	       if !check then error "Introduction needs a product"
 	       else anomaly "Intro_replacing: expects a product")
@@ -341,13 +357,13 @@ let prim_refiner r sigma goal =
     | { name = Fix; hypspecs = []; terms = []; 
 	newids = [f]; params = [Num(_,n)] } ->
      	let rec check_ind k cl = 
-          match whd_castapp cl with 
-            | DOP2(Prod,c1,DLAM(_,b)) -> 
+          match kind_of_term (whd_castapp cl) with 
+            | IsProd (_,c1,b) -> 
             	if k = 1 then 
-		  (try 
-		     let _ = find_minductype env sigma c1 in ()
-		   with Induc -> 
-		     error "cannot do a fixpoint on a non inductive type")
+		  try 
+		    let _ = find_minductype env sigma c1 in ()
+		  with Induc -> 
+		    error "cannot do a fixpoint on a non inductive type"
             	else 
 		  check_ind (k-1) b
             | _ -> error "not enough products"
@@ -361,13 +377,13 @@ let prim_refiner r sigma goal =
     
     | { name = Fix; hypspecs = []; terms = lar; newids = lf; params = ln } ->
      	let rec check_ind k cl = 
-          match whd_castapp cl with 
-            | DOP2(Prod,c1,DLAM(_,b)) -> 
+          match kind_of_term (whd_castapp cl) with 
+            | IsProd (_,c1,b) -> 
             	if k = 1 then 
-		  (try 
-		     fst (find_minductype env sigma c1)
-		   with Induc -> 
-		     error "cannot do a fixpoint on a non inductive type")
+		  try 
+		    fst (find_minductype env sigma c1)
+		  with Induc -> 
+		    error "cannot do a fixpoint on a non inductive type"
             	else 
 		  check_ind (k-1) b
             | _ -> error "not enough products"
@@ -392,14 +408,15 @@ let prim_refiner r sigma goal =
 
     | { name = Cofix; hypspecs = []; terms = lar; newids = lf; params = [] } ->
      	let rec check_is_coind cl = 
-          match (whd_betadeltaiota env sigma (whd_castapp cl)) with 
-            | DOP2(Prod,c1,DLAM(_,b)) -> check_is_coind  b
-            | b  -> 
-		(try 
-		   let _ = find_mcoinductype env sigma b in ()
-                 with Induc -> 
-		   error ("All methods must construct elements " ^
-			  "in coinductive types"))
+	  let b = whd_betadeltaiota env sigma (whd_castapp cl) in
+          match kind_of_term b with
+            | IsProd (_,c1,b) -> check_is_coind  b
+            | _ -> 
+		try 
+		  let _ = find_mcoinductype env sigma b in ()
+                with Induc -> 
+		  error ("All methods must construct elements " ^
+			  "in coinductive types")
 	in
      	List.iter check_is_coind (cl::lar);
         let rec mk_env env = function 
@@ -416,17 +433,6 @@ let prim_refiner r sigma goal =
      	in 
 	mk_env env (cl::lar,lf)
 
-(*        let rec mk_sign sign = function 
-          | (ar::lar'),(f::lf') ->
-	      if (mem_sign sign f) then 
-		error "name already used in the environment";
-	      let a = get_assumption_of env sigma ar in
-	      mk_sign (add_var_decl (f,a) sign) (lar',lf')
-	  | ([],[]) -> List.map (mk_goal info env) (cl::lar)
-	  | _ -> error "not the right number of arguments"
-     	in 
-	mk_sign sign (cl::lar,lf)*)
-	  
     | { name = Refine; terms = [c] } ->
 	let c = new_meta_variables c in
 	let (sgl,cl') = mk_refgoals sigma goal [] cl c in
@@ -436,7 +442,7 @@ let prim_refiner r sigma goal =
     | { name = Convert_concl; terms = [cl'] } ->
     	let cl'ty = type_of env sigma cl' in
 	if is_conv_leq env sigma cl' cl then
-          let sg = mk_goal info env (DOP2(Cast,cl',cl'ty)) in
+          let sg = mk_goal info env (mkCast (cl',cl'ty)) in
           [sg]
 	else 
 	  error "convert-concl rule passed non-converting term"
@@ -468,30 +474,31 @@ let prim_extractor subfun vl pft =
   let cl = pft.goal.evar_concl in
   match pft with
     | { ref = Some (Prim { name = Intro; newids = [id] }, [spf]) } ->
-	(match strip_outer_cast cl with
-	   | DOP2(Prod,ty,b) ->
+	(match kind_of_term (strip_outer_cast cl) with
+	   | IsProd (_,ty,_) ->
 	       let cty = subst_vars vl ty in
-	       DOP2(Lambda,cty, DLAM(Name id,subfun (id::vl) spf))
+	       mkLambda (Name id, cty, subfun (id::vl) spf)
 	   | _ -> error "incomplete proof!")
 	
     | { ref = Some (Prim { name = Intro_after; newids = [id]}, [spf]) } -> 
-	(match strip_outer_cast cl with
-	   | DOP2(Prod,ty,b) ->
+	(match kind_of_term (strip_outer_cast cl) with
+	   | IsProd (_,ty,_) ->
 	       let cty = subst_vars vl ty in
-	       DOP2(Lambda,cty, DLAM(Name id,subfun (id::vl) spf))
+	       mkLambda (Name id, cty, subfun (id::vl) spf)
 	   | _ -> error "incomplete proof!")
 	
     | {ref=Some(Prim{name=Intro_replacing;hypspecs=[id]},[spf]) } ->
-	(match strip_outer_cast cl with
-	   | DOP2(Prod,ty,b) ->
+	(match kind_of_term (strip_outer_cast cl) with
+	   | IsProd (_,ty,_) ->
 	       let cty = subst_vars vl ty in
-	       DOP2(Lambda,cty,DLAM(Name id,subfun (id::vl) spf))
+	       mkLambda (Name id, cty, subfun (id::vl) spf)
 	   | _ -> error "incomplete proof!")
 	
     | {ref=Some(Prim{name=Fix;newids=[f];params=[Num(_,n)]},[spf]) } -> 
 	let cty = subst_vars vl cl in 
 	let na = Name f in 
-	DOPN(Term.Fix([|n-1|],0),[| cty ; DLAMV(na,[|subfun (f::vl) spf|])|])
+	mkFix (([|n-1|],0),([|cty|], [na], [|subfun (f::vl) spf|]))
+
     | {ref=Some(Prim{name=Fix;newids=lf;terms=lar;params=ln},spfl) } ->
 	let lcty = List.map (subst_vars vl) (cl::lar) in 
 	let vn = 
diff --git a/proofs/pfedit.ml b/proofs/pfedit.ml
index 6bea1e819..c660b35ef 100644
--- a/proofs/pfedit.ml
+++ b/proofs/pfedit.ml
@@ -5,7 +5,7 @@ open Pp
 open Util
 open Names
 open Sign
-open Generic
+(*i open Generic i*)
 open Term
 open Declarations
 open Environ
diff --git a/proofs/refiner.ml b/proofs/refiner.ml
index 333287b3e..badf6bc7a 100644
--- a/proofs/refiner.ml
+++ b/proofs/refiner.ml
@@ -4,7 +4,7 @@
 open Pp
 open Util
 open Stamps
-open Generic
+(*i open Generic i*)
 open Term
 open Sign
 open Evd
@@ -271,7 +271,7 @@ let extract_open_proof sigma pf =
 	let ass = Retyping.get_assumption_of goal.evar_env sigma abs_concl in
 	let mv = new_meta() in
 	open_obligations := (mv,ass):: !open_obligations;
-	applist(DOP0(Meta mv),List.map (fun (n,_) -> Rel n) sorted_rels) 
+	applist (mkMeta mv, List.map (fun (n,_) -> mkRel n) sorted_rels) 
 	  
     | _ -> anomaly "Bug : a case has been forgotten in proof_extractor"
   in
diff --git a/proofs/tacinterp.ml b/proofs/tacinterp.ml
index 1feb14508..28eaa7ad4 100644
--- a/proofs/tacinterp.ml
+++ b/proofs/tacinterp.ml
@@ -3,7 +3,7 @@
 
 open Astterm
 open Closure
-open Generic
+(*i open Generic i*)
 open Libobject
 open Pattern
 open Pp
diff --git a/proofs/tacmach.ml b/proofs/tacmach.ml
index 1488b06de..e8d4be64e 100644
--- a/proofs/tacmach.ml
+++ b/proofs/tacmach.ml
@@ -4,7 +4,7 @@
 open Util
 open Stamps
 open Names
-open Generic
+(*i open Generic i*)
 open Sign
 open Term
 open Instantiate
@@ -104,7 +104,7 @@ let pf_reduce_to_ind            = pf_reduce reduce_to_ind
 let hnf_type_of gls = compose (pf_whd_betadeltaiota gls) (pf_type_of gls)
 
 let pf_check_type gls c1 c2 =
-  let casted = mkCast c1 c2 in pf_type_of gls casted
+  let casted = mkCast (c1, c2) in pf_type_of gls casted
 
 (************************************)
 (* Tactics handling a list of goals *)
diff --git a/proofs/tacmach.mli b/proofs/tacmach.mli
index bf2b0a3ba..e6130c3f6 100644
--- a/proofs/tacmach.mli
+++ b/proofs/tacmach.mli
@@ -191,8 +191,8 @@ val walking_THEN        : 'a result_w_tactic -> ('a -> tactic) -> tactic
 val walking             : w_tactic -> tactic
 val w_Focusing_THEN     : int -> 'a result_w_tactic 
                           -> ('a -> w_tactic) -> w_tactic
-val w_Declare           : int -> constr -> w_tactic
-val w_Declare_At        : int -> int -> constr -> w_tactic
+val w_Declare           : int -> constr * constr -> w_tactic
+val w_Declare_At        : int -> int -> constr * constr -> w_tactic
 val w_Define            : int -> constr -> w_tactic
 val w_Underlying        : walking_constraints -> evar_declarations
 val w_env               : walking_constraints -> env