diff options
| author |  herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2003-09-06 19:12:08 +0000 |
|---|---|---|
| committer | herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2003-09-06 19:12:08 +0000 |
| commit | 95d4aef96fb7b490b188afe66e8345428e9706ee (patch) | |
| tree | 3990c1a6bfce095e941d756df5387b63e86e8353 /contrib/xml/acic.ml | |
| parent | ef41c3d1f93e2fa82cbaa97adaa03852e8fcd7b8 (diff) | |
Paramétrisation vis à vis de existential_key
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4321 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'contrib/xml/acic.ml')
| -rw-r--r-- | contrib/xml/acic.ml | 6 |
1 files changed, 3 insertions, 3 deletions
diff --git a/contrib/xml/acic.ml b/contrib/xml/acic.ml index 693b7cb3c..36541a57d 100644 --- a/contrib/xml/acic.ml +++ b/contrib/xml/acic.ml @@ -23,7 +23,7 @@ type 'constr context_entry = type 'constr hypothesis = identifier * 'constr context_entry type context = constr hypothesis list -type conjecture = int * context * constr +type conjecture = existential_key * context * constr type metasenv = conjecture list (* list of couples section path -- variables defined in that section *) @@ -51,7 +51,7 @@ and constructor = type aconstr = | ARel of id * int * id * identifier | AVar of id * uri - | AEvar of id * int * aconstr list + | AEvar of id * existential_key * aconstr list | ASort of id * sorts | ACast of id * aconstr * aconstr | AProds of (id * name * aconstr) list * aconstr @@ -71,7 +71,7 @@ and acoinductivefun = and explicit_named_substitution = id option * (uri * aconstr) list type acontext = (id * aconstr hypothesis) list -type aconjecture = id * int * acontext * aconstr +type aconjecture = id * existential_key * acontext * aconstr type ametasenv = aconjecture list type aobj = |