nouvelle implantation de la reduction

suppression de IsXtra du noyau


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

8 files changed, 456 insertions, 11 deletions

diff --git a/pretyping/cbv.ml b/pretyping/cbv.ml
new file mode 100644
index 000000000..15a50bcc4
--- /dev/null
+++ b/pretyping/cbv.ml
@@ -0,0 +1,396 @@
+
+(* $Id$ *)
+
+open Util
+open Pp
+open Term
+open Names
+open Environ
+open Instantiate
+open Univ
+open Evd
+open Closure
+open Esubst
+
+(**** Call by value reduction ****)
+
+(* The type of terms with closure. The meaning of the constructors and
+ * the invariants of this datatype are the following:
+ *  VAL(k,c) represents the constr c with a delayed shift of k. c must be
+ *          in normal form and neutral (i.e. not a lambda, a construct or a
+ *          (co)fix, because they may produce redexes by applying them,
+ *          or putting them in a case)
+ *  LAM(x,a,b,S) is the term [S]([x:a]b). the substitution is propagated
+ *          only when the abstraction is applied, and then we use the rule
+ *                  ([S]([x:a]b) c) --> [S.c]b
+ *          This corresponds to the usual strategy of weak reduction
+ *  FIXP(op,bd,S,args) is the fixpoint (Fix or Cofix) of bodies bd under
+ *          the substitution S, and then applied to args. Here again,
+ *          weak reduction.
+ *  CONSTR(n,(sp,i),vars,args) is the n-th constructor of the i-th
+ *          inductive type sp.
+ *
+ * Note that any term has not an equivalent in cbv_value: for example,
+ * a product (x:A)B must be in normal form because only VAL may
+ * represent it, and the argument of VAL is always in normal
+ * form. This remark precludes coding a head reduction with these
+ * functions. Anyway, does it make sense to head reduce with a
+ * call-by-value strategy ?
+ *)
+type cbv_value =
+  | VAL of int * constr
+  | LAM of name * constr * constr * cbv_value subs
+  | FIXP of fixpoint * cbv_value subs * cbv_value list
+  | COFIXP of cofixpoint * cbv_value subs * cbv_value list
+  | CONSTR of int * inductive_path * cbv_value array * cbv_value list
+
+(* les vars pourraient etre des constr,
+   cela permet de retarder les lift: utile ?? *) 
+
+(* relocation of a value; used when a value stored in a context is expanded
+ * in a larger context. e.g.  [%k (S.t)](k+1) --> [^k]t  (t is shifted of k)
+ *)
+let rec shift_value n = function
+  | VAL (k,v) -> VAL ((k+n),v)
+  | LAM (x,a,b,s) -> LAM (x,a,b,subs_shft (n,s))
+  | FIXP (fix,s,args) ->
+      FIXP (fix,subs_shft (n,s), List.map (shift_value n) args)
+  | COFIXP (cofix,s,args) ->
+      COFIXP (cofix,subs_shft (n,s), List.map (shift_value n) args)
+  | CONSTR (i,spi,vars,args) ->
+      CONSTR (i, spi, Array.map (shift_value n) vars,
+              List.map (shift_value n) args)
+	
+
+(* Contracts a fixpoint: given a fixpoint and a substitution,
+ * returns the corresponding fixpoint body, and the substitution in which
+ * it should be evaluated: its first variables are the fixpoint bodies
+ * (S, (fix Fi {F0 := T0 .. Fn-1 := Tn-1}))
+ *    -> (S. [S]F0 . [S]F1 ... . [S]Fn-1, Ti)
+ *)
+let contract_fixp env ((reci,i),(_,_,bds as bodies)) =
+  let make_body j = FIXP(((reci,j),bodies), env, []) in
+  let n = Array.length bds in
+  let rec subst_bodies_from_i i subs =
+    if i=n then subs
+    else subst_bodies_from_i (i+1) (subs_cons (make_body i, subs))
+  in       
+  subst_bodies_from_i 0 env, bds.(i)
+
+let contract_cofixp env (i,(_,_,bds as bodies)) =
+  let make_body j = COFIXP((j,bodies), env, []) in
+  let n = Array.length bds in
+  let rec subst_bodies_from_i i subs =
+    if i=n then subs
+    else subst_bodies_from_i (i+1) (subs_cons (make_body i, subs))
+  in       
+  subst_bodies_from_i 0 env, bds.(i)
+
+
+(* type of terms with a hole. This hole can appear only under App or Case.
+ *   TOP means the term is considered without context
+ *   APP(l,stk) means the term is applied to l, and then we have the context st
+ *      this corresponds to the application stack of the KAM.
+ *      The members of l are values: we evaluate arguments before the function.
+ *   CASE(t,br,pat,S,stk) means the term is in a case (which is himself in stk
+ *      t is the type of the case and br are the branches, all of them under
+ *      the subs S, pat is information on the patterns of the Case
+ *      (Weak reduction: we propagate the sub only when the selected branch
+ *      is determined)
+ *
+ * Important remark: the APPs should be collapsed:
+ *    (APP (l,(APP ...))) forbidden
+ *)
+
+type cbv_stack =
+  | TOP
+  | APP of cbv_value list * cbv_stack
+  | CASE of constr * constr array * case_info * cbv_value subs * cbv_stack
+
+(* Adds an application list. Collapse APPs! *)
+let stack_app appl stack =
+  match (appl, stack) with
+    | ([], _)            -> stack
+    | (_, APP(args,stk)) -> APP(appl@args,stk)
+    | _                  -> APP(appl, stack)
+
+(* Tests if we are in a case (modulo some applications) *)
+let under_case_stack = function
+  | (CASE _ | APP(_,CASE _)) -> true
+  | _ -> false
+
+(* Tells if the reduction rk is allowed by flags under a given stack.
+ * The stack is useful when flags is (SIMPL,r) because in that case,
+ * we perform bdi-reduction under the Case, or r-reduction otherwise
+ *)
+let red_allowed flags stack rk =
+  if under_case_stack stack then 
+    red_under flags rk
+  else 
+    red_top flags rk
+
+let red_allowed_ref flags stack = function
+  | FarRelBinding _ -> red_allowed flags stack DELTA
+  | VarBinding id -> red_allowed flags stack (VAR id)
+  | EvarBinding _ -> red_allowed flags stack EVAR
+  | ConstBinding (sp,_) -> red_allowed flags stack (CONST [sp])
+
+(* Transfer application lists from a value to the stack
+ * useful because fixpoints may be totally applied in several times
+ *)
+let strip_appl head stack =
+  match head with
+    | FIXP (fix,env,app) -> (FIXP(fix,env,[]), stack_app app stack)
+    | COFIXP (cofix,env,app) -> (COFIXP(cofix,env,[]), stack_app app stack)
+    | CONSTR (i,spi,vars,app) -> (CONSTR(i,spi,vars,[]), stack_app app stack)
+    | _ -> (head, stack)
+
+
+(* Invariant: if the result of norm_head is CONSTR or (CO)FIXP, its last
+ * argument is [].
+ * Because we must put all the applied terms in the stack.
+ *)
+let reduce_const_body redfun v stk =
+  if under_case_stack stk then strip_appl (redfun v) stk else strip_appl v stk
+ 
+
+(* Tests if fixpoint reduction is possible. A reduction function is given as
+   argument *)
+let rec check_app_constr redfun = function
+  | ([], _) -> false
+  | ((CONSTR _)::_, 0) -> true
+  | (t::_, 0) -> (* TODO: partager ce calcul *)
+      (match redfun t with
+         | CONSTR _ -> true
+         | _ -> false)
+  | (_::l, n) -> check_app_constr redfun (l,(pred n))
+	
+let fixp_reducible redfun flgs ((reci,i),_) stk =
+  if red_allowed flgs stk IOTA then
+    match stk with               (* !!! for Acc_rec: reci.(i) = -2 *)
+      | APP(appl,_) -> reci.(i) >=0 & check_app_constr redfun (appl, reci.(i))
+      | _ -> false
+  else 
+    false
+
+let cofixp_reducible redfun flgs _ stk =
+  if red_allowed flgs stk IOTA then
+    match stk with
+      | (CASE _ | APP(_,CASE _)) -> true
+      | _ -> false
+  else 
+    false
+
+let mindsp_nparams env (sp,i) =
+  let mib = lookup_mind sp env in
+  (Declarations.mind_nth_type_packet mib i).Declarations.mind_nparams
+
+(* The main recursive functions
+ *
+ * Go under applications and cases (pushed in the stack), expand head
+ * constants or substitued de Bruijn, and try to make appear a
+ * constructor, a lambda or a fixp in the head. If not, it is a value
+ * and is completely computed here. The head redexes are NOT reduced:
+ * the function returns the pair of a cbv_value and its stack.  *
+ * Invariant: if the result of norm_head is CONSTR or (CO)FIXP, it last
+ * argument is [].  Because we must put all the applied terms in the
+ * stack. *)
+
+let rec norm_head info env t stack =
+  (* no reduction under binders *)
+  match kind_of_term t with
+  (* stack grows (remove casts) *)
+  | IsApp (head,args) -> (* Applied terms are normalized immediately;
+                        they could be computed when getting out of the stack *)
+      let nargs = Array.map (cbv_stack_term info TOP env) args in
+      norm_head info env head (stack_app (Array.to_list nargs) stack)
+  | IsMutCase (ci,p,c,v) -> norm_head info env c (CASE(p,v,ci,env,stack))
+  | IsCast (ct,_) -> norm_head info env ct stack
+
+  (* constants, axioms
+   * the first pattern is CRUCIAL, n=0 happens very often:
+   * when reducing closed terms, n is always 0 *)
+  | IsRel i -> (match expand_rel i env with
+                | Inl (0,v) ->
+                    reduce_const_body (cbv_norm_more info env) v stack
+                | Inl (n,v) ->
+                    reduce_const_body
+                      (cbv_norm_more info env) (shift_value n v) stack
+                | Inr (n,None) ->
+		    (VAL(0, mkRel n), stack)
+                | Inr (n,Some p) ->
+		    norm_head_ref (n-p) info env stack (FarRelBinding p))
+
+  | IsVar id -> norm_head_ref 0 info env stack (VarBinding id)
+
+  | IsConst (sp,vars) ->
+      let normt = (sp,Array.map (cbv_norm_term info env) vars) in
+      norm_head_ref 0 info env stack (ConstBinding normt)
+
+  | IsEvar ev -> norm_head_ref 0 info env stack (EvarBinding (ev,env))
+
+  | IsLetIn (x, b, t, c) ->
+      (* zeta means letin are contracted; delta without zeta means we *)
+      (* allow substitution but leave let's in place *)
+      let zeta = red_allowed (info_flags info) stack ZETA in
+      let env' =
+	if zeta or red_allowed (info_flags info) stack DELTA then 
+	  subs_cons (cbv_stack_term info TOP env b,env)
+	else
+	  subs_lift env in
+      if zeta then
+        norm_head info env' c stack
+      else
+	let normt =
+	  mkLetIn (x, cbv_norm_term info env b,
+		   cbv_norm_term info env t,
+		   cbv_norm_term info env' c) in
+	(VAL(0,normt), stack) (* Considérer une coupure commutative ? *)
+
+  (* non-neutral cases *)
+  | IsLambda (x,a,b) -> (LAM(x,a,b,env), stack)
+  | IsFix fix -> (FIXP(fix,env,[]), stack)
+  | IsCoFix cofix -> (COFIXP(cofix,env,[]), stack)
+  | IsMutConstruct ((spi,i),vars) ->
+      (CONSTR(i,spi, Array.map (cbv_stack_term info TOP env) vars,[]), stack)
+
+  (* neutral cases *)
+  | (IsSort _ | IsMeta _) -> (VAL(0, t), stack)
+  | IsMutInd (sp,vars) -> 
+      (VAL(0, mkMutInd (sp, Array.map (cbv_norm_term info env) vars)), stack)
+  | IsProd (x,t,c) -> 
+      (VAL(0, mkProd (x, cbv_norm_term info env t,
+		      cbv_norm_term info (subs_lift env) c)),
+	     stack)
+
+and norm_head_ref k info env stack normt =
+  if red_allowed_ref (info_flags info) stack normt then
+    match ref_value_cache info normt with
+      | Some body ->
+	  reduce_const_body (cbv_norm_more info env) (shift_value k body) stack
+      | None -> (VAL(0,make_constr_ref k info normt), stack)
+  else (VAL(0,make_constr_ref k info normt), stack)
+
+and make_constr_ref n info = function
+  | FarRelBinding p -> mkRel (n+p)
+  | VarBinding id -> mkVar id
+  | EvarBinding ((ev,args),env) ->
+      mkEvar (ev,Array.map (cbv_norm_term info env) args)
+  | ConstBinding cst -> mkConst cst
+
+(* cbv_stack_term performs weak reduction on constr t under the subs
+ * env, with context stack, i.e. ([env]t stack).  First computes weak
+ * head normal form of t and checks if a redex appears with the stack.
+ * If so, recursive call to reach the real head normal form.  If not,
+ * we build a value. 
+ *)
+and cbv_stack_term info stack env t =
+  match norm_head info env t stack with
+    (* a lambda meets an application -> BETA *)
+    | (LAM (x,a,b,env), APP (arg::args, stk))
+      when red_allowed (info_flags info) stk BETA ->
+        let subs = subs_cons (arg,env) in
+          cbv_stack_term info (stack_app args stk) subs b
+
+    (* a Fix applied enough -> IOTA *)
+    | (FIXP(fix,env,_), stk)
+        when fixp_reducible (cbv_norm_more info env) (info_flags info) fix stk ->
+        let (envf,redfix) = contract_fixp env fix in
+        cbv_stack_term info stk envf redfix
+
+    (* constructor guard satisfied or Cofix in a Case -> IOTA *)
+    | (COFIXP(cofix,env,_), stk)
+        when cofixp_reducible (cbv_norm_more info env) (info_flags info) cofix stk->
+        let (envf,redfix) = contract_cofixp env cofix in
+        cbv_stack_term info stk envf redfix
+
+    (* constructor in a Case -> IOTA
+       (use red_under because we know there is a Case) *)
+    | (CONSTR(n,sp,_,_), APP(args,CASE(_,br,(arity,_),env,stk)))
+            when red_under (info_flags info) IOTA ->
+	let ncargs = arity.(n-1) in
+	let real_args = list_lastn ncargs args in
+        cbv_stack_term info (stack_app real_args stk) env br.(n-1)
+         
+    (* constructor of arity 0 in a Case -> IOTA ( "   " )*)
+    | (CONSTR(n,_,_,_), CASE(_,br,_,env,stk))
+                  when red_under (info_flags info) IOTA ->
+                    cbv_stack_term info stk env br.(n-1)
+
+    (* may be reduced later by application *)  
+    | (head, TOP) -> head
+    | (FIXP(fix,env,_), APP(appl,TOP)) -> FIXP(fix,env,appl) 
+    | (COFIXP(cofix,env,_), APP(appl,TOP)) -> COFIXP(cofix,env,appl) 
+    | (CONSTR(n,spi,vars,_), APP(appl,TOP)) -> CONSTR(n,spi,vars,appl)
+
+    (* definitely a value *)
+    | (head,stk) -> VAL(0,apply_stack info (cbv_norm_value info head) stk)
+
+
+(* if we are in SIMPL mode, maybe v isn't reduced enough *)
+and cbv_norm_more info env v =
+  match (v, (info_flags info)) with
+    | (VAL(k,t), ((SIMPL|WITHBACK),_)) ->
+        cbv_stack_term (infos_under info) TOP (subs_shft (k,env)) t
+    | _ -> v
+
+
+(* When we are sure t will never produce a redex with its stack, we
+ * normalize (even under binders) the applied terms and we build the
+ * final term
+ *)
+and apply_stack info t = function
+  | TOP -> t
+  | APP (args,st) ->
+      apply_stack info (applistc t (List.map (cbv_norm_value info) args)) st
+  | CASE (ty,br,ci,env,st) ->
+      apply_stack info
+        (mkMutCase (ci, cbv_norm_term info env ty, t,
+		    Array.map (cbv_norm_term info env) br))
+        st
+
+
+(* performs the reduction on a constr, and returns a constr *)
+and cbv_norm_term info env t =
+  (* reduction under binders *)
+  cbv_norm_value info (cbv_stack_term info TOP env t)
+
+(* reduction of a cbv_value to a constr *)
+and cbv_norm_value info = function (* reduction under binders *)
+  | VAL (n,v) -> lift n v
+  | LAM (x,a,b,env) ->
+      mkLambda (x, cbv_norm_term info env a,
+		cbv_norm_term info (subs_lift env) b)
+  | FIXP ((lij,(lty,lna,bds)),env,args) ->
+      applistc
+        (mkFix (lij,
+		(Array.map (cbv_norm_term info env) lty, lna, 
+		 Array.map (cbv_norm_term info 
+			      (subs_liftn (Array.length lty) env)) bds)))
+        (List.map (cbv_norm_value info) args)
+  | COFIXP ((j,(lty,lna,bds)),env,args) ->
+      applistc
+        (mkCoFix (j,
+		  (Array.map (cbv_norm_term info env) lty, lna, 
+		   Array.map (cbv_norm_term info 
+				(subs_liftn (Array.length lty) env)) bds)))
+        (List.map (cbv_norm_value info) args)
+  | CONSTR (n,spi,vars,args) ->
+      applistc
+        (mkMutConstruct ((spi,n), Array.map (cbv_norm_value info) vars))
+        (List.map (cbv_norm_value info) args)
+
+(* with profiling *)
+let cbv_norm infos constr =
+  with_stats (lazy (cbv_norm_term infos (ESID 0) constr))
+
+
+type 'a cbv_infos = (cbv_value, 'a) infos
+
+(* constant bodies are normalized at the first expansion *)
+let create_cbv_infos flgs env sigma =
+  create
+    (fun old_info s c -> cbv_stack_term old_info TOP s c)
+    flgs
+    env
+    sigma
diff --git a/pretyping/cbv.mli b/pretyping/cbv.mli
new file mode 100644
index 000000000..08e067f5a
--- /dev/null
+++ b/pretyping/cbv.mli
@@ -0,0 +1,55 @@
+
+(*i $Id$ i*)
+
+(*i*)
+open Pp
+open Names
+open Term
+open Evd
+open Environ
+open Closure
+open Esubst
+(*i*)
+
+(***********************************************************************)
+(*s Call-by-value reduction *)
+
+(* Entry point for cbv normalization of a constr *)
+type 'a cbv_infos
+val create_cbv_infos : flags -> env -> 'a evar_map -> 'a cbv_infos
+val cbv_norm : 'a cbv_infos -> constr -> constr
+
+(***********************************************************************)
+(*i This is for cbv debug *)
+type cbv_value =
+  | VAL of int * constr
+  | LAM of name * constr * constr * cbv_value subs
+  | FIXP of fixpoint * cbv_value subs * cbv_value list
+  | COFIXP of cofixpoint * cbv_value subs * cbv_value list
+  | CONSTR of int * (section_path * int) * cbv_value array * cbv_value list
+
+val shift_value : int -> cbv_value -> cbv_value
+
+type cbv_stack =
+  | TOP
+  | APP of cbv_value list * cbv_stack
+  | CASE of constr * constr array * case_info * cbv_value subs * cbv_stack
+
+val stack_app : cbv_value list -> cbv_stack -> cbv_stack
+val under_case_stack : cbv_stack -> bool
+val strip_appl : cbv_value -> cbv_stack -> cbv_value * cbv_stack
+
+val red_allowed : flags -> cbv_stack -> red_kind -> bool
+val reduce_const_body :
+  (cbv_value -> cbv_value) -> cbv_value -> cbv_stack -> cbv_value * cbv_stack
+
+(* recursive functions... *)
+val cbv_stack_term : 'a cbv_infos ->
+  cbv_stack -> cbv_value subs -> constr -> cbv_value
+val cbv_norm_term : 'a cbv_infos -> cbv_value subs -> constr -> constr
+val cbv_norm_more : 'a cbv_infos -> cbv_value subs -> cbv_value -> cbv_value
+val norm_head : 'a cbv_infos ->
+  cbv_value subs -> constr -> cbv_stack -> cbv_value * cbv_stack
+val apply_stack : 'a cbv_infos -> constr -> cbv_stack -> constr
+val cbv_norm_value : 'a cbv_infos -> cbv_value -> constr
+(* End of cbv debug section i*)
diff --git a/pretyping/detyping.ml b/pretyping/detyping.ml
index dc4330b5e..e376abb25 100644
--- a/pretyping/detyping.ml
+++ b/pretyping/detyping.ml
@@ -283,9 +283,6 @@ let rec detype avoid env t =
 	 in RVar (dummy_loc, id_of_string s))
     | IsMeta n -> RMeta (dummy_loc, n)
     | IsVar id -> RVar (dummy_loc, id)
-    | IsXtra s -> warning "bdize: Xtra should no longer occur in constr";
-	RVar(dummy_loc, id_of_string ("XTRA"^s))
-        (* ope("XTRA",((str s):: pl@(List.map detype cl)))*) 
     | IsSort (Prop c) -> RSort (dummy_loc,RProp c)
     | IsSort (Type _) -> RSort (dummy_loc,RType)
     | IsCast (c1,c2) ->
diff --git a/pretyping/evarconv.ml b/pretyping/evarconv.ml
index 8dab70441..82746d287 100644
--- a/pretyping/evarconv.ml
+++ b/pretyping/evarconv.ml
@@ -257,8 +257,8 @@ and evar_eqappr_x env isevars pbty (term1,l1 as appr1) (term2,l2 as appr2) =
 		 bds1 bds2)
 	    & (list_for_all2eq (evar_conv_x env isevars CONV) l1 l2)
 
-	| (IsMeta _ | IsXtra _ | IsLambda _), _ -> false
-	| _, (IsMeta _ | IsXtra _ | IsLambda _) -> false
+	| (IsMeta _ | IsLambda _), _ -> false
+	| _, (IsMeta _ | IsLambda _) -> false
 
 	| (IsMutInd _ | IsMutConstruct _ | IsSort _ | IsProd _), _ -> false
 	| _, (IsMutInd _ | IsMutConstruct _ | IsSort _ | IsProd _) -> false
diff --git a/pretyping/pattern.ml b/pretyping/pattern.ml
index 625e28d56..b83019b45 100644
--- a/pretyping/pattern.ml
+++ b/pretyping/pattern.ml
@@ -269,7 +269,7 @@ let rec sub_match nocc pat c =
       let (lm,le) = try_sub_match (nocc - 1) pat (c1::Array.to_list lc) in
       (lm,mkMutCaseL (ci,hd,List.hd le,List.tl le)))
   | IsMutConstruct _ | IsFix _ | IsMutInd _|IsCoFix _ |IsEvar _|IsConst _
-  | IsRel _|IsMeta _|IsVar _|IsXtra _|IsSort _ ->
+  | IsRel _|IsMeta _|IsVar _|IsSort _ ->
     (try authorized_occ nocc ((matches pat c),mkMeta (-1)) with
     | PatternMatchingFailure -> raise (NextOccurrence nocc)
     | NextOccurrence nocc -> raise (NextOccurrence (nocc - 1)))
@@ -320,7 +320,6 @@ let rec pattern_of_constr t =
     | IsFix f -> PFix f
     | IsCoFix _ ->
 	error "pattern_of_constr: (co)fix currently not supported"
-    | IsXtra _   -> anomaly "No longer supported"
 
 and pattern_of_ref ref inst =
   let args = Declare.extract_instance ref inst in
diff --git a/pretyping/retyping.ml b/pretyping/retyping.ml
index ee8c1f764..657f3d1e0 100644
--- a/pretyping/retyping.ml
+++ b/pretyping/retyping.ml
@@ -73,7 +73,6 @@ let rec type_of env cstr=
 			  (Array.to_list args))
     | IsCast (c,t) -> t
     | IsSort _ | IsProd (_,_,_) | IsMutInd _ -> mkSort (sort_of env cstr)
-    | IsXtra _ -> error "type_of: Unexpected constr"
 
 and sort_of env t = 
   match kind_of_term t with
diff --git a/pretyping/tacred.ml b/pretyping/tacred.ml
index baf120029..1b4b89f8b 100644
--- a/pretyping/tacred.ml
+++ b/pretyping/tacred.ml
@@ -10,6 +10,7 @@ open Environ
 open Reduction
 open Closure
 open Instantiate
+open Cbv
 
 (************************************************************************)
 (* Reduction of constant hiding fixpoints (e.g. for Simpl). The trick   *)
@@ -584,7 +585,7 @@ let rec substlin env name n ol c =
     | IsCoFix _ -> 
         (warning "do not consider occurrences inside cofixpoints"; (n,ol,c))
 
-    | (IsRel _|IsMeta _|IsVar _|IsXtra _|IsSort _
+    | (IsRel _|IsMeta _|IsVar _|IsSort _
       |IsEvar _|IsConst _|IsMutInd _|IsMutConstruct _) -> (n,ol,c)
 	
 let unfold env sigma name =
diff --git a/pretyping/typing.ml b/pretyping/typing.ml
index d3f7eb0ed..afdaf5823 100644
--- a/pretyping/typing.ml
+++ b/pretyping/typing.ml
@@ -115,8 +115,6 @@ let rec execute mf env sigma cstr =
         let j, _ = cast_rel env sigma cj tj in
 	j
 	  
-    | IsXtra _ -> anomaly "Typing: found an Extra"
-	  
 and execute_fix mf env sigma lar lfi vdef =
   let larj = execute_array mf env sigma lar in
   let lara = Array.map (assumption_of_judgment env sigma) larj in