diff options
| author |  Emilio Jesus Gallego Arias <e+git@x80.org> | 2017-05-24 17:24:46 +0200 |
|---|---|---|
| committer | Emilio Jesus Gallego Arias <e+git@x80.org> | 2017-05-24 17:41:21 +0200 |
| commit | 6f2c19a1054ce58927dfa5b33131c3665fd5fdf8 (patch) | |
| tree | b8a60ea2387f14a415d53a3cd9db516e384a5b4f /vernac/auto_ind_decl.ml | |
| parent | a02f76f38592fd84cabd34102d38412f046f0d1b (diff) | |
| parent | 28f8da9489463b166391416de86420c15976522f (diff) | |
Merge branch 'trunk' into located_switch
Diffstat (limited to 'vernac/auto_ind_decl.ml')
| -rw-r--r-- | vernac/auto_ind_decl.ml | 8 |
1 files changed, 2 insertions, 6 deletions
diff --git a/vernac/auto_ind_decl.ml b/vernac/auto_ind_decl.ml index fd454b67e..31d610abd 100644 --- a/vernac/auto_ind_decl.ml +++ b/vernac/auto_ind_decl.ml @@ -9,7 +9,6 @@ (* This file is about the automatic generation of schemes about decidable equality, created by Vincent Siles, Oct 2007 *) -open Tacmach open CErrors open Util open Pp @@ -28,8 +27,6 @@ open Proofview.Notations module RelDecl = Context.Rel.Declaration -let out_punivs = Univ.out_punivs - (**********************************************************************) (* Generic synthesis of boolean equality *) @@ -93,7 +90,7 @@ let destruct_on_using c id = let destruct_on_as c l = destruct false None c (Some (Loc.tag l)) None -(* reconstruct the inductive with the correct deBruijn indexes *) +(* reconstruct the inductive with the correct de Bruijn indexes *) let mkFullInd (ind,u) n = let mib = Global.lookup_mind (fst ind) in let nparams = mib.mind_nparams in @@ -172,7 +169,7 @@ let build_beq_scheme mode kn = (* give a type A, this function tries to find the equality on A declared previously *) (* nlist = the number of args (A , B , ... ) - eqA = the deBruijn index of the first eq param + eqA = the de Bruijn index of the first eq param ndx = how much to translate due to the 2nd Case *) let compute_A_equality rel_list nlist eqA ndx t = @@ -716,7 +713,6 @@ let compute_lb_goal ind lnamesparrec nparrec = ))), eff let compute_lb_tact mode lb_scheme_key ind lnamesparrec nparrec = - let open EConstr in let list_id = list_id lnamesparrec in let avoid = ref [] in let first_intros = |