alim of now resets the counter

diff --git a/helm/ocaml/cic_proof_checking/cicElim.ml b/helm/ocaml/cic_proof_checking/cicElim.ml
index 707a7b2b2ed522886791f670aacb7d21af1787fb..c0552e79ee7385c38bbf3f0781c8895eab8897e3 100644 (file)
--- a/helm/ocaml/cic_proof_checking/cicElim.ml
+++ b/helm/ocaml/cic_proof_checking/cicElim.ml
@@ -30,8 +30,9 @@ exception Can_t_eliminate
 
 let debug_print = fun _ -> ()
 
+let counter = ref ~-1 ;;
+
 let fresh_binder =
-  let counter = ref ~-1 in
   function
     | true ->
         incr counter;
@@ -243,6 +244,7 @@ let branch (uri, typeno) insource liftno paramsno t fix head args =
   branch (uri, typeno) insource paramsno t fix head args
 
 let elim_of ?(sort = Cic.Type (CicUniv.fresh ())) uri typeno =
+  counter := ~-1;
   let (obj, univ) = (CicEnvironment.get_obj CicUniv.empty_ugraph uri) in
   match obj with
   | Cic.InductiveDefinition (indTypes, params, leftno, _) ->