diff options
| author |  filliatr <filliatr@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2000-12-12 22:07:41 +0000 |
|---|---|---|
| committer | filliatr <filliatr@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2000-12-12 22:07:41 +0000 |
| commit | 8030a420d2cfcf8372d5fe6544efbecde940381b (patch) | |
| tree | 6d4a3c198d4dbecf0cf15f3b53c31447aacfafd7 /kernel | |
| parent | faa2647739aa33421328af4ffeaba1bb474e868e (diff) | |
syntaxe AST Inversion + commentaires ocamlweb autour de $
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1090 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'kernel')
| -rw-r--r-- | kernel/closure.mli | 2 | ||||
| -rw-r--r-- | kernel/declarations.mli | 2 | ||||
| -rw-r--r-- | kernel/environ.mli | 2 | ||||
| -rw-r--r-- | kernel/evd.mli | 2 | ||||
| -rw-r--r-- | kernel/indtypes.mli | 2 | ||||
| -rw-r--r-- | kernel/inductive.mli | 2 | ||||
| -rw-r--r-- | kernel/instantiate.mli | 2 | ||||
| -rw-r--r-- | kernel/names.mli | 2 | ||||
| -rw-r--r-- | kernel/reduction.mli | 2 | ||||
| -rw-r--r-- | kernel/safe_typing.ml | 3 | ||||
| -rw-r--r-- | kernel/safe_typing.mli | 2 | ||||
| -rw-r--r-- | kernel/sign.mli | 2 | ||||
| -rw-r--r-- | kernel/term.ml | 6 | ||||
| -rw-r--r-- | kernel/term.mli | 2 | ||||
| -rw-r--r-- | kernel/type_errors.mli | 2 | ||||
| -rw-r--r-- | kernel/typeops.mli | 2 | ||||
| -rw-r--r-- | kernel/univ.mli | 2 |
17 files changed, 20 insertions, 19 deletions
diff --git a/kernel/closure.mli b/kernel/closure.mli index b546942e1..c38c6aaa0 100644 --- a/kernel/closure.mli +++ b/kernel/closure.mli @@ -1,5 +1,5 @@ -(* $Id$ *) +(*i $Id$ i*) (*i*) open Pp diff --git a/kernel/declarations.mli b/kernel/declarations.mli index 3e7d8a9bd..0cc927c8c 100644 --- a/kernel/declarations.mli +++ b/kernel/declarations.mli @@ -1,5 +1,5 @@ -(* $Id$ *) +(*i $Id$ i*) (*i*) open Names diff --git a/kernel/environ.mli b/kernel/environ.mli index 14209cd72..eb6a45480 100644 --- a/kernel/environ.mli +++ b/kernel/environ.mli @@ -1,5 +1,5 @@ -(* $Id$ *) +(*i $Id$ i*) (*i*) open Names diff --git a/kernel/evd.mli b/kernel/evd.mli index 6ab60e295..2353b6789 100644 --- a/kernel/evd.mli +++ b/kernel/evd.mli @@ -1,5 +1,5 @@ -(* $Id$ *) +(*i $Id$ i*) (*i*) open Names diff --git a/kernel/indtypes.mli b/kernel/indtypes.mli index 00e108460..71041c279 100644 --- a/kernel/indtypes.mli +++ b/kernel/indtypes.mli @@ -1,5 +1,5 @@ -(* $Id$ *) +(*i $Id$ i*) (*i*) open Names diff --git a/kernel/inductive.mli b/kernel/inductive.mli index 054a7d3fe..547979fde 100644 --- a/kernel/inductive.mli +++ b/kernel/inductive.mli @@ -1,5 +1,5 @@ -(* $Id$ *) +(*i $Id$ i*) (*i*) open Names diff --git a/kernel/instantiate.mli b/kernel/instantiate.mli index 9f790e3ca..a80dcc435 100644 --- a/kernel/instantiate.mli +++ b/kernel/instantiate.mli @@ -1,5 +1,5 @@ -(* $Id$ *) +(*i $Id$ i*) (*i*) open Names diff --git a/kernel/names.mli b/kernel/names.mli index cca174463..afdcd3a54 100644 --- a/kernel/names.mli +++ b/kernel/names.mli @@ -1,5 +1,5 @@ -(* $Id$ *) +(*i $Id$ i*) (*i*) open Pp diff --git a/kernel/reduction.mli b/kernel/reduction.mli index 10b4edc43..7828ff940 100644 --- a/kernel/reduction.mli +++ b/kernel/reduction.mli @@ -1,5 +1,5 @@ -(* $Id$ *) +(*i $Id$ i*) (*i*) open Names diff --git a/kernel/safe_typing.ml b/kernel/safe_typing.ml index 642673a8a..c0e700a13 100644 --- a/kernel/safe_typing.ml +++ b/kernel/safe_typing.ml @@ -312,6 +312,7 @@ let add_discharged_constant sp r env = | None -> add_parameter sp typ env | Some c -> + (* let c = hcons1_constr c in *) let (jtyp,cst) = safe_infer env typ in let env' = add_constraints cst env in let ids = @@ -319,7 +320,7 @@ let add_discharged_constant sp r env = (global_vars_set (body_of_type jtyp.uj_val)) in let cb = { const_kind = kind_of_path sp; - const_body = body; + const_body = Some c; const_type = assumption_of_judgment env' Evd.empty jtyp; const_hyps = keep_hyps ids (named_context env); const_constraints = cst; diff --git a/kernel/safe_typing.mli b/kernel/safe_typing.mli index 011d0e414..7f50c7104 100644 --- a/kernel/safe_typing.mli +++ b/kernel/safe_typing.mli @@ -1,5 +1,5 @@ -(* $Id$ *) +(*i $Id$ i*) (*i*) open Pp diff --git a/kernel/sign.mli b/kernel/sign.mli index 38d058042..5c93bccbf 100644 --- a/kernel/sign.mli +++ b/kernel/sign.mli @@ -1,5 +1,5 @@ -(* $Id$ *) +(*i $Id$ i*) (*i*) open Names diff --git a/kernel/term.ml b/kernel/term.ml index ff96a8e15..7a3c7e053 100644 --- a/kernel/term.ml +++ b/kernel/term.ml @@ -1668,10 +1668,10 @@ let hcons_constr (hspcci,hspfw,hname,hident,hstr) = let htcci = Hashcons.simple_hcons Htype.f (hcci,hsortscci) in (hcci,hfw,htcci) -let hcons1_constr c = - let hnames = hcons_names() in +let hcons1_constr = + let hnames = hcons_names () in let (hc,_,_) = hcons_constr hnames in - hc c + hc (* Abstract decomposition of constr to deal with generic functions *) diff --git a/kernel/term.mli b/kernel/term.mli index d4dbd8ce1..bbd02b6e6 100644 --- a/kernel/term.mli +++ b/kernel/term.mli @@ -1,5 +1,5 @@ -(* $Id$ *) +(*i $Id$ i*) (*i*) open Util diff --git a/kernel/type_errors.mli b/kernel/type_errors.mli index 68628c63c..670a9f5de 100644 --- a/kernel/type_errors.mli +++ b/kernel/type_errors.mli @@ -1,5 +1,5 @@ -(* $Id$ *) +(*i $Id$ i*) (*i*) open Pp diff --git a/kernel/typeops.mli b/kernel/typeops.mli index d51594822..6e5cdca3e 100644 --- a/kernel/typeops.mli +++ b/kernel/typeops.mli @@ -1,5 +1,5 @@ -(* $Id$ *) +(*i $Id$ i*) (*i*) open Names diff --git a/kernel/univ.mli b/kernel/univ.mli index ba0b6aea1..2460ff15e 100644 --- a/kernel/univ.mli +++ b/kernel/univ.mli @@ -1,5 +1,5 @@ -(* $Id$ *) +(*i $Id$ i*) (*i*) open Names |