[checker] Refactor by sharing code with the kernel

For historical reasons, the checker was duplicating a lot of code of the
kernel. The main differences I found were bug fixes that had not been
backported.

With this patch, the checker uses the kernel as a library to serve the
same purpose as before: validation of a `.vo` file, re-typechecking all
definitions a posteriori.

We also rename some files from the checker so that they don't clash with
kernel files.

1 files changed, 0 insertions, 627 deletions

diff --git a/checker/reduction.ml b/checker/reduction.ml
deleted file mode 100644
index 1158152f63..0000000000
--- a/checker/reduction.ml
+++ /dev/null
@@ -1,627 +0,0 @@
-(************************************************************************)
-(*         *   The Coq Proof Assistant / The Coq Development Team       *)
-(*  v      *   INRIA, CNRS and contributors - Copyright 1999-2018       *)
-(* <O___,, *       (see CREDITS file for the list of authors)           *)
-(*   \VV/  **************************************************************)
-(*    //   *    This file is distributed under the terms of the         *)
-(*         *     GNU Lesser General Public License Version 2.1          *)
-(*         *     (see LICENSE file for the text of the license)         *)
-(************************************************************************)
-
-open Names
-open CErrors
-open Util
-open Cic
-open Term
-open Closure
-open Esubst
-open Environ
-
-let rec is_empty_stack = function
-    [] -> true
-  | Zupdate _::s -> is_empty_stack s
-  | Zshift _::s -> is_empty_stack s
-  | _ -> false
-
-(* Compute the lift to be performed on a term placed in a given stack *)
-let el_stack el stk =
-  let n =
-    List.fold_left
-      (fun i z ->
-        match z with
-            Zshift n -> i+n
-          | _ -> i)
-      0
-      stk in
-  el_shft n el
-
-let compare_stack_shape stk1 stk2 =
-  let rec compare_rec bal stk1 stk2 =
-  match (stk1,stk2) with
-      ([],[]) -> bal=0
-    | ((Zupdate _|Zshift _)::s1, _) -> compare_rec bal s1 stk2
-    | (_, (Zupdate _|Zshift _)::s2) -> compare_rec bal stk1 s2
-    | (Zapp l1::s1, _) -> compare_rec (bal+Array.length l1) s1 stk2
-    | (_, Zapp l2::s2) -> compare_rec (bal-Array.length l2) stk1 s2
-    | (Zproj p1::s1, Zproj p2::s2) ->
-        Int.equal bal 0 && compare_rec 0 s1 s2
-    | ((ZcaseT(c1,_,_,_))::s1,
-       (ZcaseT(c2,_,_,_))::s2) ->
-        bal=0 (* && c1.ci_ind  = c2.ci_ind *) && compare_rec 0 s1 s2
-    | (Zfix(_,a1)::s1, Zfix(_,a2)::s2) ->
-        bal=0 && compare_rec 0 a1 a2 && compare_rec 0 s1 s2
-    | (_,_) -> false in
-  compare_rec 0 stk1 stk2
-
-type lft_constr_stack_elt =
-    Zlapp of (lift * fconstr) array
-  | Zlproj of Names.Projection.Repr.t * lift
-  | Zlfix of (lift * fconstr) * lft_constr_stack
-  | Zlcase of case_info * lift * fconstr * fconstr array
-and lft_constr_stack = lft_constr_stack_elt list
-
-let rec zlapp v = function
-    Zlapp v2 :: s -> zlapp (Array.append v v2) s
-  | s -> Zlapp v :: s
-
-let pure_stack lfts stk =
-  let rec pure_rec lfts stk =
-    match stk with
-        [] -> (lfts,[])
-      | zi::s ->
-          (match (zi,pure_rec lfts s) with
-              (Zupdate _,lpstk)  -> lpstk
-            | (Zshift n,(l,pstk)) -> (el_shft n l, pstk)
-            | (Zapp a, (l,pstk)) ->
-                (l,zlapp (Array.map (fun t -> (l,t)) a) pstk)
-            | (Zproj p, (l,pstk)) ->
-                (l, Zlproj (p,l)::pstk)
-            | (Zfix(fx,a),(l,pstk)) ->
-                let (lfx,pa) = pure_rec l a in
-                (l, Zlfix((lfx,fx),pa)::pstk)
-            | (ZcaseT(ci,p,br,env),(l,pstk)) ->
-                (l,Zlcase(ci,l,mk_clos env p,mk_clos_vect env br)::pstk)
-            ) in
-  snd (pure_rec lfts stk)
-
-(****************************************************************************)
-(*                   Reduction Functions                                    *)
-(****************************************************************************)
-
-let whd_betaiotazeta x =
-  match x with
-    | (Sort _|Var _|Meta _|Evar _|Const _|Ind _|Construct _|
-       Prod _|Lambda _|Fix _|CoFix _) -> x
-    | _ -> whd_val (create_clos_infos betaiotazeta empty_env) (inject x)
-
-let whd_all env t =
-  match t with
-    | (Sort _|Meta _|Evar _|Ind _|Construct _|
-       Prod _|Lambda _|Fix _|CoFix _) -> t
-    | _ -> whd_val (create_clos_infos betadeltaiota env) (inject t)
-
-let whd_allnolet env t =
-  match t with
-    | (Sort _|Meta _|Evar _|Ind _|Construct _|
-       Prod _|Lambda _|Fix _|CoFix _|LetIn _) -> t
-    | _ -> whd_val (create_clos_infos betadeltaiotanolet env) (inject t)
-
-(* Beta *)
-
-let beta_appvect c v =
-  let rec stacklam env t stack =
-    match t, stack with
-        Lambda(_,_,c), arg::stacktl -> stacklam (arg::env) c stacktl
-      | _ -> applist (substl env t, stack) in
-  stacklam [] c (Array.to_list v)
-
-(********************************************************************)
-(*                         Conversion                               *)
-(********************************************************************)
-
-type conv_pb =
-  | CONV
-  | CUMUL
-
-(* Conversion utility functions *)
-type 'a conversion_function = env -> 'a -> 'a -> unit
-
-exception NotConvertible
-exception NotConvertibleVect of int
-
-let convert_universes univ u u' =
-  if Univ.Instance.check_eq univ u u' then ()
-  else raise NotConvertible
-
-let compare_stacks f fmind fproj lft1 stk1 lft2 stk2 =
-  let rec cmp_rec pstk1 pstk2 =
-    match (pstk1,pstk2) with
-      | (z1::s1, z2::s2) ->
-          cmp_rec s1 s2;
-          (match (z1,z2) with
-            | (Zlapp a1,Zlapp a2) -> Array.iter2 f a1 a2
-            | (Zlfix(fx1,a1),Zlfix(fx2,a2)) ->
-                f fx1 fx2; cmp_rec a1 a2
-	    | (Zlproj (c1,l1),Zlproj (c2,l2)) -> 
-               if not (fproj c1 c2) then
-                raise NotConvertible
-            | (Zlcase(ci1,l1,p1,br1),Zlcase(ci2,l2,p2,br2)) ->
-                if not (fmind ci1.ci_ind ci2.ci_ind) then
-		  raise NotConvertible;
-		f (l1,p1) (l2,p2);
-                Array.iter2 (fun c1 c2 -> f (l1,c1) (l2,c2)) br1 br2
-            | _ -> assert false)
-      | _ -> () in
-  if compare_stack_shape stk1 stk2 then
-    cmp_rec (pure_stack lft1 stk1) (pure_stack lft2 stk2)
-  else raise NotConvertible
-
-let convert_inductive_instances cv_pb cumi u u' univs =
-  let len_instance =
-      Univ.AUContext.size (Univ.ACumulativityInfo.univ_context cumi) in
-  if not ((len_instance = Univ.Instance.length u) &&
-          (len_instance = Univ.Instance.length u')) then
-    anomaly (Pp.str "Invalid inductive subtyping encountered!")
-  else
-    let variance = Univ.ACumulativityInfo.variance cumi in
-    let comp_cst =
-      match cv_pb with
-      | CONV ->
-        Univ.Variance.eq_constraints variance u u' Univ.Constraint.empty
-      | CUMUL ->
-        Univ.Variance.leq_constraints variance u u' Univ.Constraint.empty
-    in
-    if (Univ.check_constraints comp_cst univs) then () else raise NotConvertible
-
-let convert_inductives
-    cv_pb (mind, ind) u1 sv1 u2 sv2 univs =
-  match mind.mind_universes with
-  | Monomorphic_ind _ | Polymorphic_ind _ -> convert_universes univs u1 u2
-  | Cumulative_ind cumi ->
-    let num_param_arity =
-      mind.mind_nparams + mind.mind_packets.(ind).mind_nrealargs
-    in
-    if not (num_param_arity = sv1 && num_param_arity = sv2) then
-      convert_universes univs u1 u2
-    else
-      convert_inductive_instances cv_pb cumi u1 u2 univs
-
-let convert_constructors
-    (mind, ind, cns) u1 sv1 u2 sv2 univs =
-  match mind.mind_universes with
-  | Monomorphic_ind _ | Polymorphic_ind _ -> convert_universes univs u1 u2
-  | Cumulative_ind cumi ->
-    let num_cnstr_args =
-      mind.mind_nparams + mind.mind_packets.(ind).mind_consnrealargs.(cns - 1)
-    in
-    if not (num_cnstr_args = sv1 && num_cnstr_args = sv2) then
-      convert_universes univs u1 u2
-    else
-      (** By invariant, both constructors have a common supertype,
-          so they are convertible _at that type_. *)
-      ()
-
-(* Convertibility of sorts *)
-
-let sort_cmp env univ pb s0 s1 =
-  match (s0,s1) with
-  | Prop, Prop | Set, Set -> ()
-  | Prop, (Set | Type _) | Set, Type _ ->
-    if not (pb = CUMUL) then raise NotConvertible
-  | Type u1, Type u2 ->
-    (** FIXME: handle type-in-type option here *)
-    if (* snd (engagement env) == StratifiedType && *)
-      not
-        (match pb with
-         | CONV -> Univ.check_eq univ u1 u2
-         | CUMUL -> Univ.check_leq univ u1 u2)
-    then begin
-      if !Flags.debug then begin
-        let op = match pb with CONV -> "=" | CUMUL -> "<=" in
-        Format.eprintf "sort_cmp: @[%a@]\n%!" Pp.pp_with Pp.(
-            str"Error: " ++ Univ.pr_uni u1 ++ str op ++ Univ.pr_uni u2 ++ str ":" ++ cut()
-            ++ Univ.pr_universes univ)
-      end;
-      raise NotConvertible
-    end
-  | Set, Prop | Type _, (Prop | Set) -> raise NotConvertible
-
-let rec no_arg_available = function
-  | [] -> true
-  | Zupdate _ :: stk -> no_arg_available stk
-  | Zshift _ :: stk -> no_arg_available stk
-  | Zapp v :: stk -> Array.length v = 0 && no_arg_available stk
-  | Zproj _ :: _ -> true
-  | ZcaseT _ :: _ -> true
-  | Zfix _ :: _ -> true
-
-let rec no_nth_arg_available n = function
-  | [] -> true
-  | Zupdate _ :: stk -> no_nth_arg_available n stk
-  | Zshift _ :: stk -> no_nth_arg_available n stk
-  | Zapp v :: stk ->
-      let k = Array.length v in
-      if n >= k then no_nth_arg_available (n-k) stk
-      else false
-  | Zproj _ :: _ -> true
-  | ZcaseT _ :: _ -> true
-  | Zfix _ :: _ -> true
-
-let rec no_case_available = function
-  | [] -> true
-  | Zupdate _ :: stk -> no_case_available stk
-  | Zshift _ :: stk -> no_case_available stk
-  | Zapp _ :: stk -> no_case_available stk
-  | Zproj _ :: _ -> false
-  | ZcaseT _ :: _ -> false
-  | Zfix _ :: _ -> true
-
-let in_whnf (t,stk) =
-  match fterm_of t with
-    | (FLetIn _ | FCaseT _ | FApp _ | FCLOS _ | FLIFT _ | FCast _) -> false
-    | FLambda _ -> no_arg_available stk
-    | FConstruct _ -> no_case_available stk
-    | FCoFix _ -> no_case_available stk
-    | FFix(((ri,n),(_,_,_)),_) -> no_nth_arg_available ri.(n) stk
-    | (FFlex _ | FProd _ | FEvar _ | FInd _ | FAtom _ | FRel _ | FProj _) -> true
-    | FLOCKED -> assert false
-
-let default_level = Level 0
-
-let get_strategy { var_opacity; cst_opacity } = function
-  | VarKey id ->
-      (try Names.Id.Map.find id var_opacity
-      with Not_found -> default_level)
-  | ConstKey (c, _) ->
-      (try Names.Cmap.find c cst_opacity
-      with Not_found -> default_level)
-  | RelKey _ -> Expand
-
-let dep_order l2r k1 k2 = match k1, k2 with
-| RelKey _, RelKey _ -> l2r
-| RelKey _, (VarKey _ | ConstKey _) -> true
-| VarKey _, RelKey _ -> false
-| VarKey _, VarKey _ -> l2r
-| VarKey _, ConstKey _ -> true
-| ConstKey _, (RelKey _ | VarKey _) -> false
-| ConstKey _, ConstKey _ -> l2r
-
-let oracle_order infos l2r k1 k2 =
-  let o = Closure.oracle_of_infos infos in
-  match get_strategy o k1, get_strategy o k2 with
-  | Expand, Expand -> dep_order l2r k1 k2
-  | Expand, (Opaque | Level _) -> true
-  | (Opaque | Level _), Expand -> false
-  | Opaque, Opaque -> dep_order l2r k1 k2
-  | Level _, Opaque -> true
-  | Opaque, Level _ -> false
-  | Level n1, Level n2 ->
-     if Int.equal n1 n2 then dep_order l2r k1 k2
-     else n1 < n2
-
-let eq_table_key univ =
-  Names.eq_table_key (fun (c1,u1) (c2,u2) ->
-      Constant.UserOrd.equal c1 c2 &&
-      Univ.Instance.check_eq univ u1 u2)
-
-let proj_equiv_infos infos p1 p2 =
-  Int.equal (Projection.Repr.arg p1) (Projection.Repr.arg p2) &&
-  mind_equiv (infos_env infos) (Projection.Repr.inductive p1) (Projection.Repr.inductive p2)
-
-(* Conversion between  [lft1]term1 and [lft2]term2 *)
-let rec ccnv univ cv_pb infos lft1 lft2 term1 term2 =
-  eqappr univ cv_pb infos (lft1, (term1,[])) (lft2, (term2,[]))
-
-(* Conversion between [lft1](hd1 v1) and [lft2](hd2 v2) *)
-and eqappr univ cv_pb infos (lft1,st1) (lft2,st2) =
-  Control.check_for_interrupt ();
-  (* First head reduce both terms *)
-  let rec whd_both (t1,stk1) (t2,stk2) =
-    let st1' = whd_stack infos t1 stk1 in
-    let st2' = whd_stack infos t2 stk2 in
-    (* Now, whd_stack on term2 might have modified st1 (due to sharing),
-       and st1 might not be in whnf anymore. If so, we iterate ccnv. *)
-    if in_whnf st1' then (st1',st2') else whd_both st1' st2' in
-  let ((hd1,v1),(hd2,v2)) = whd_both st1 st2 in
-  let appr1 = (lft1,(hd1,v1)) and appr2 = (lft2,(hd2,v2)) in
-  (* compute the lifts that apply to the head of the term (hd1 and hd2) *)
-  let el1 = el_stack lft1 v1 in
-  let el2 = el_stack lft2 v2 in
-  match (fterm_of hd1, fterm_of hd2) with
-    (* case of leaves *)
-    | (FAtom a1, FAtom a2) ->
-	(match a1, a2 with
-	   | (Sort s1, Sort s2) ->
-	       assert (is_empty_stack v1 && is_empty_stack v2);
-	       sort_cmp (infos_env infos) univ cv_pb s1 s2
-	   | (Meta n, Meta m) ->
-               if n=m
-	       then convert_stacks univ infos lft1 lft2 v1 v2
-               else raise NotConvertible
-	   | _ -> raise NotConvertible)
-    | (FEvar (ev1,args1), FEvar (ev2,args2)) ->
-        if ev1=ev2 then
-          (convert_stacks univ infos lft1 lft2 v1 v2;
-           convert_vect univ infos el1 el2 args1 args2)
-        else raise NotConvertible
-
-    (* 2 index known to be bound to no constant *)
-    | (FRel n, FRel m) ->
-        if reloc_rel n el1 = reloc_rel m el2
-        then convert_stacks univ infos lft1 lft2 v1 v2
-        else raise NotConvertible
-
-    (* 2 constants, 2 local defined vars or 2 defined rels *)
-    | (FFlex fl1, FFlex fl2) ->
-	(try (* try first intensional equality *)
-          if eq_table_key univ fl1 fl2
-          then convert_stacks univ infos lft1 lft2 v1 v2
-          else raise NotConvertible
-        with NotConvertible ->
-          (* else the oracle tells which constant is to be expanded *)
-          let (app1,app2) =
-            if oracle_order infos false fl1 fl2 then
-              match unfold_reference infos fl1 with
-              | Some def1 -> ((lft1, whd_stack infos def1 v1), appr2)
-              | None ->
-                (match unfold_reference infos fl2 with
-                | Some def2 -> (appr1, (lft2, whd_stack infos def2 v2))
-                | None -> raise NotConvertible)
-            else
-	      match unfold_reference infos fl2 with
-              | Some def2 -> (appr1, (lft2, whd_stack infos def2 v2))
-              | None ->
-                (match unfold_reference infos fl1 with
-                | Some def1 -> ((lft1, whd_stack infos def1 v1), appr2)
-		| None -> raise NotConvertible) in
-            eqappr univ cv_pb infos app1 app2)
-	  
-    | (FProj (p1,c1), _) ->
-      let s1 = unfold_projection (infos_env infos) p1 in
-        eqappr univ cv_pb infos (lft1, whd_stack infos c1 (s1 :: v1)) appr2
-	  
-    | (_, FProj (p2,c2)) ->
-      let s2 = unfold_projection (infos_env infos) p2 in
-        eqappr univ cv_pb infos appr1 (lft2, whd_stack infos c2 (s2 :: v2))
-
-    (* other constructors *)
-    | (FLambda _, FLambda _) ->
-        (* Inconsistency: we tolerate that v1, v2 contain shift and update but
-           we throw them away *)
-        assert (is_empty_stack v1 && is_empty_stack v2);
-        let (_,ty1,bd1) = destFLambda mk_clos hd1 in
-        let (_,ty2,bd2) = destFLambda mk_clos hd2 in
-        ccnv univ CONV infos el1 el2 ty1 ty2;
-        ccnv univ CONV infos (el_lift el1) (el_lift el2) bd1 bd2
-
-    | (FProd (_,c1,c2), FProd (_,c'1,c'2)) ->
-        assert (is_empty_stack v1 && is_empty_stack v2);
-	(* Luo's system *)
-        ccnv univ CONV infos el1 el2 c1 c'1;
-        ccnv univ cv_pb infos (el_lift el1) (el_lift el2) c2 c'2
-
-    (* Eta-expansion on the fly *)
-    | (FLambda _, _) ->
-        if v1 <> [] then
-          anomaly (Pp.str "conversion was given unreduced term (FLambda).");
-        let (_,_ty1,bd1) = destFLambda mk_clos hd1 in
-        eqappr univ CONV infos
-          (el_lift lft1,(bd1,[])) (el_lift lft2,(hd2,eta_expand_stack v2))
-    | (_, FLambda _) ->
-        if v2 <> [] then
-          anomaly (Pp.str "conversion was given unreduced term (FLambda).");
-        let (_,_ty2,bd2) = destFLambda mk_clos hd2 in
-        eqappr univ CONV infos
-          (el_lift lft1,(hd1,eta_expand_stack v1)) (el_lift lft2,(bd2,[]))
-
-    (* only one constant, defined var or defined rel *)
-    | (FFlex fl1, c2)      ->
-        (match unfold_reference infos fl1 with
-           | Some def1 ->
-	       eqappr univ cv_pb infos (lft1, whd_stack infos def1 v1) appr2
-           | None -> 
-	     match c2 with 
-	     | FConstruct ((ind2,j2),u2) ->
-	       (try
- 	     	  let v2, v1 = 
- 		    eta_expand_ind_stack (infos_env infos) ind2 hd2 v2 (snd appr1)
- 		  in convert_stacks univ infos lft1 lft2 v1 v2
- 	     	with Not_found -> raise NotConvertible)
-	     | _ -> raise NotConvertible)
-
-    | (c1, FFlex fl2)      ->
-        (match unfold_reference infos fl2 with
-           | Some def2 ->
-	       eqappr univ cv_pb infos appr1 (lft2, whd_stack infos def2 v2)
-           | None -> 
-	     match c1 with 
-	     | FConstruct ((ind1,j1),u1) ->
- 	       (try let v1, v2 = 
-		      eta_expand_ind_stack (infos_env infos) ind1 hd1 v1 (snd appr2)
-		    in convert_stacks univ infos lft1 lft2 v1 v2
-		with Not_found -> raise NotConvertible)
-	     | _ -> raise NotConvertible)
-
-    (* Inductive types:  MutInd MutConstruct Fix Cofix *)
-
-    | (FInd (ind1,u1), FInd (ind2,u2)) ->
-      if mind_equiv_infos infos ind1 ind2 then
-        if Univ.Instance.length u1 = 0 || Univ.Instance.length u2 = 0 then
-          begin
-            convert_universes univ u1 u2;
-            convert_stacks univ infos lft1 lft2 v1 v2
-          end
-        else
-          let mind = Environ.lookup_mind (fst ind1) (infos_env infos) in
-          let () =
-            convert_inductives cv_pb (mind, snd ind1) u1 (stack_args_size v1)
-              u2 (stack_args_size v2) univ
-          in
-          convert_stacks univ infos lft1 lft2 v1 v2
-      else raise NotConvertible
-
-    | (FConstruct ((ind1,j1),u1), FConstruct ((ind2,j2),u2)) ->
-      if Int.equal j1 j2 && mind_equiv_infos infos ind1 ind2 then
-        if Univ.Instance.length u1 = 0 || Univ.Instance.length u2 = 0 then
-          begin
-            convert_universes univ u1 u2;
-            convert_stacks univ infos lft1 lft2 v1 v2
-          end
-        else
-          let mind = Environ.lookup_mind (fst ind1) (infos_env infos) in
-          let () =
-            convert_constructors
-              (mind, snd ind1, j1) u1 (stack_args_size v1)
-              u2 (stack_args_size v2) univ
-          in
-          convert_stacks univ infos lft1 lft2 v1 v2
-      else raise NotConvertible
-
-     (* Eta expansion of records *)
-     | (FConstruct ((ind1,j1),u1), _) ->
-       (try
-    	  let v1, v2 =
-    	    eta_expand_ind_stack (infos_env infos) ind1 hd1 v1 (snd appr2)
-    	  in convert_stacks univ infos lft1 lft2 v1 v2
-	with Not_found -> raise NotConvertible)
-	 
-     | (_, FConstruct ((ind2,j2),u2)) ->
-       (try
-    	  let v2, v1 =
-    	    eta_expand_ind_stack (infos_env infos) ind2 hd2 v2 (snd appr1)
-    	  in convert_stacks univ infos lft1 lft2 v1 v2
-	with Not_found -> raise NotConvertible)
-
-     | (FFix ((op1,(_,tys1,cl1)),e1), FFix((op2,(_,tys2,cl2)),e2)) ->
-	 if op1 = op2
-	 then
-	   let n = Array.length cl1 in
-           let fty1 = Array.map (mk_clos e1) tys1 in
-           let fty2 = Array.map (mk_clos e2) tys2 in
-           let fcl1 = Array.map (mk_clos (subs_liftn n e1)) cl1 in
-           let fcl2 = Array.map (mk_clos (subs_liftn n e2)) cl2 in
-           convert_vect univ infos el1 el2 fty1 fty2;
-           convert_vect univ infos
-	     (el_liftn n el1) (el_liftn n el2) fcl1 fcl2;
-           convert_stacks univ infos lft1 lft2 v1 v2
-         else raise NotConvertible
-
-     | (FCoFix ((op1,(_,tys1,cl1)),e1), FCoFix((op2,(_,tys2,cl2)),e2)) ->
-         if op1 = op2
-         then
-	   let n = Array.length cl1 in
-           let fty1 = Array.map (mk_clos e1) tys1 in
-           let fty2 = Array.map (mk_clos e2) tys2 in
-           let fcl1 = Array.map (mk_clos (subs_liftn n e1)) cl1 in
-           let fcl2 = Array.map (mk_clos (subs_liftn n e2)) cl2 in
-           convert_vect univ infos el1 el2 fty1 fty2;
-	   convert_vect univ infos
-	     (el_liftn n el1) (el_liftn n el2) fcl1 fcl2;
-           convert_stacks univ infos lft1 lft2 v1 v2
-         else raise NotConvertible
-
-     (* Should not happen because both (hd1,v1) and (hd2,v2) are in whnf *)
-     | ( (FLetIn _, _) | (FCaseT _,_) | (FApp _,_) | (FCLOS _,_) | (FLIFT _,_)
-       | (_, FLetIn _) | (_,FCaseT _) | (_,FApp _) | (_,FCLOS _) | (_,FLIFT _)
-       | (FLOCKED,_) | (_,FLOCKED) ) -> assert false
-
-     (* In all other cases, terms are not convertible *)
-     | _ -> raise NotConvertible
-
-and convert_stacks univ infos lft1 lft2 stk1 stk2 =
-  compare_stacks
-    (fun (l1,t1) (l2,t2) -> ccnv univ CONV infos l1 l2 t1 t2)
-    (mind_equiv_infos infos) (proj_equiv_infos infos)
-    lft1 stk1 lft2 stk2
-
-and convert_vect univ infos lft1 lft2 v1 v2 =
-  Array.iter2 (fun t1 t2 -> ccnv univ CONV infos lft1 lft2 t1 t2) v1 v2
-
-let clos_fconv cv_pb eager_delta env t1 t2 =
-  let infos =
-    create_clos_infos
-      (if eager_delta then betadeltaiota else betaiotazeta) env in
-  let univ = universes env in
-  ccnv univ cv_pb infos el_id el_id (inject t1) (inject t2)
-
-let fconv cv_pb eager_delta env t1 t2 =
-  if eq_constr t1 t2 then ()
-  else clos_fconv cv_pb eager_delta env t1 t2
-
-let conv = fconv CONV false
-let conv_leq = fconv CUMUL false
-
-(* option for conversion : no compilation for the checker *)
-
-let vm_conv cv_pb = fconv cv_pb true
-
-(********************************************************************)
-(*             Special-Purpose Reduction                            *)
-(********************************************************************)
-
-(* pseudo-reduction rule:
- * [hnf_prod_app env s (Prod(_,B)) N --> B[N]
- * with an HNF on the first argument to produce a product.
- * if this does not work, then we use the string S as part of our
- * error message. *)
-
-let hnf_prod_app env t n =
-  match whd_all env t with
-    | Prod (_,_,b) -> subst1 n b
-    | _ -> anomaly ~label:"hnf_prod_app" (Pp.str "Need a product.")
-
-let hnf_prod_applist env t nl =
-  List.fold_left (hnf_prod_app env) t nl
-
-(* Dealing with arities *)
-
-let dest_prod env =
-  let rec decrec env m c =
-    let t = whd_all env c in
-    match t with
-      | Prod (n,a,c0) ->
-          let d = LocalAssum (n,a) in
-	  decrec (push_rel d env) (d::m) c0
-      | _ -> m,t
-  in
-  decrec env empty_rel_context
-
-(* The same but preserving lets in the context, not internal ones. *)
-let dest_prod_assum env =
-  let rec prodec_rec env l ty =
-    let rty = whd_allnolet env ty in
-    match rty with
-    | Prod (x,t,c)  ->
-        let d = LocalAssum (x,t) in
-	prodec_rec (push_rel d env) (d::l) c
-    | LetIn (x,b,t,c) ->
-        let d = LocalDef (x,b,t) in
-	prodec_rec (push_rel d env) (d::l) c
-    | _               ->
-      let rty' = whd_all env rty in
-	if Term.eq_constr rty' rty then l, rty
-	else prodec_rec env l rty'
-  in
-  prodec_rec env empty_rel_context
-
-let dest_lam_assum env =
-  let rec lamec_rec env l ty =
-    let rty = whd_allnolet env ty in
-    match rty with
-    | Lambda (x,t,c)  ->
-        let d = LocalAssum (x,t) in
-	lamec_rec (push_rel d env) (d::l) c
-    | LetIn (x,b,t,c) ->
-        let d = LocalDef (x,b,t) in
-	lamec_rec (push_rel d env) (d::l) c
-    | _               -> l,rty
-  in
-  lamec_rec env empty_rel_context
-
-
-let dest_arity env c =
-  let l, c = dest_prod_assum env c in
-  match c with
-    | Sort s -> l,s
-    | _ -> user_err Pp.(str "not an arity")
-