diff options
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 dc9b01b17b..e6d44eb45a 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 11e621acf7..ff592ed944 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 |