From fc38a7d8f3d2a47aa8eee570747568335f3ffa19 Mon Sep 17 00:00:00 2001 From: delahaye Date: Wed, 3 May 2000 17:31:07 +0000 Subject: Ajout du langage de tactiques git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@401 85f007b7-540e-0410-9357-904b9bb8a0f7 --- kernel/environ.ml | 9 ++++----- 1 file changed, 4 insertions(+), 5 deletions(-) (limited to 'kernel/environ.ml') diff --git a/kernel/environ.ml b/kernel/environ.ml index fdfc540d26..4471d5b873 100644 --- a/kernel/environ.ml +++ b/kernel/environ.ml @@ -103,10 +103,10 @@ let add_abstraction sp ab env = env_abstractions = new_abs; env_locals = new_locals } in { env with env_globals = new_globals } - -let new_meta = - let meta_ctr = ref 0 in - fun () -> (incr meta_ctr; !meta_ctr) + +let meta_ctr=ref 0;; + +let new_meta ()=incr meta_ctr;!meta_ctr;; (* Access functions. *) @@ -310,4 +310,3 @@ type unsafe_judgment = { let cast_of_judgment = function | { uj_val = DOP2 (Cast,_,_) as c } -> c | { uj_val = c; uj_type = ty } -> mkCast c ty - -- cgit v1.2.3