From 14d08596263d9247b7a32bc6528f0a649e6f7908 Mon Sep 17 00:00:00 2001
From: herbelin
Date: Fri, 28 Apr 2000 19:11:52 +0000
Subject: Déplacement du type reference dans Term Découpage de tactics/pattern
 en proofs/pattern et tactics/hipattern Renommage des fonctions somatch and co
 dans Pattern et Tacticals Divers extensions pour utiliser les constr_pattern

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@383 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 kernel/term.ml | 20 +++++++++++++++++---
 1 file changed, 17 insertions(+), 3 deletions(-)

(limited to 'kernel')

diff --git a/kernel/term.ml b/kernel/term.ml
index 3ed337847d..bd14984538 100644
--- a/kernel/term.ml
+++ b/kernel/term.ml
@@ -547,16 +547,30 @@ let destUntypedCoFix = function
       (i,types,funnames,bodies)
   | _ -> invalid_arg "destCoFix"
 
+(**********************************************************************)
 
-(******************)
-(* Term analysis  *)
-(******************)
+type binder_kind = BProd | BLambda
+
+type fix_kind = RFix of int array * int | RCofix of int
+
+type 'ctxt reference =
+  | RConst of section_path * 'ctxt
+  | RInd of inductive_path * 'ctxt
+  | RConstruct of constructor_path * 'ctxt
+  | RAbst of section_path
+  | RVar of identifier
+  | REVar of int * 'ctxt
+  | RMeta of int
 
 type existential = int * constr array
 type constant = section_path * constr array
 type constructor = constructor_path * constr array
 type inductive = inductive_path * constr array
 
+(******************)
+(* Term analysis  *)
+(******************)
+
 type kindOfTerm = 
   | IsRel          of int
   | IsMeta         of int
-- 
cgit v1.2.3