From: Enrico Tassi <enrico.tassi@inria.fr>
Date: Thu, 7 Jul 2005 11:01:59 +0000 (+0000)
Subject: alim of now resets the counter
X-Git-Tag: V_0_7_1~27
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=16cfd31fa90759c8318b6bb12c992c45df60c41b;p=helm.git

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 707a7b2b2..c0552e79e 100644
--- 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, _) ->