From 79dc33cbc403ebab0bd1fe815c13f740f0a1b850 Mon Sep 17 00:00:00 2001
From: herbelin
Date: Sun, 10 Sep 2000 07:19:28 +0000
Subject: 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
---
 dev/changements.txt | 1 +
 dev/top_printers.ml | 8 ++++----
 2 files changed, 5 insertions(+), 4 deletions(-)

(limited to 'dev')

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
-- 
cgit v1.2.3