diff options
| author |  herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2000-09-10 07:19:28 +0000 |
|---|---|---|
| committer | herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2000-09-10 07:19:28 +0000 |
| commit | 79dc33cbc403ebab0bd1fe815c13f740f0a1b850 (patch) | |
| tree | e38e167003d7dd97d95a59ea7c026a1629b346f8 /dev | |
| parent | c0ff579606f2eba24bc834316d8bb7bcc076000d (diff) | |
Ajout d'un LetIn primitif.
Abstraction de constr via kind_of_constr dans une bonne partie du code.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@591 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'dev')
| -rw-r--r-- | dev/changements.txt | 1 | ||||
| -rw-r--r-- | dev/top_printers.ml | 8 |
2 files changed, 5 insertions, 4 deletions
diff --git a/dev/changements.txt b/dev/changements.txt index dc9b01b17..e6d44eb45 100644 --- a/dev/changements.txt +++ b/dev/changements.txt @@ -10,6 +10,7 @@ Changements d'organisation / modules : Avm,Mavm,Fmavm,Mhm -> utiliser plutôt Map (et freeze alors gratuit) Mhb -> Bij + Generic est intégré à Term (et un petit peu à Closure) Changements dans les types de données : --------------------------------------- diff --git a/dev/top_printers.ml b/dev/top_printers.ml index 11e621acf..ff592ed94 100644 --- a/dev/top_printers.ml +++ b/dev/top_printers.ml @@ -9,7 +9,7 @@ open Sign open Univ open Proof_trees open Environ -open Generic +(*i open Generic i*) open Printer open Refiner open Tacmach @@ -84,13 +84,13 @@ let constr_display csr = | DOPN(a,b) -> "DOPN("^(oper_display a)^",[|"^(Array.fold_right (fun x i -> (term_display x)^(if not(i="") then (";"^i) else "")) b "")^"|])" - | DOPL(a,b) -> - "DOPL("^(oper_display a)^",[|"^(List.fold_right (fun x i -> - (term_display x)^(if not(i="") then (";"^i) else "")) b "")^"|]" | DLAM(a,b) -> "DLAM("^(name_display a)^","^(term_display b)^")" | DLAMV(a,b) -> "DLAMV("^(name_display a)^",[|"^(Array.fold_right (fun x i -> (term_display x)^(if not(i="") then (";"^i) else "")) b "")^"|]" + | CLam(a,b,c) -> "CLam("^(name_display a)^","^(term_display (body_of_type b))^","^(term_display c)^")" + | CPrd(a,b,c) -> "CPrd("^(name_display a)^","^(term_display (body_of_type b))^","^(term_display c)^")" + | CLet(a,b,c,d) -> "CLet("^(name_display a)^","^(term_display b)^","^(term_display (body_of_type c))^","^(term_display d)^")" | VAR a -> "VAR "^(string_of_id a) | Rel a -> "Rel "^(string_of_int a) and oper_display = function |