From 2a07b93999a919cfe8f764a53681d0c33917c1a4 Mon Sep 17 00:00:00 2001
From: filliatr <filliatr@85f007b7-540e-0410-9357-904b9bb8a0f7>
Date: Sun, 5 Dec 1999 18:37:47 +0000
Subject: changement type add_anonymous_leaf

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@206 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 pretyping/classops.ml   | 7 ++-----
 pretyping/pretyping.mli | 3 +--
 pretyping/recordops.ml  | 9 +++------
 pretyping/syntax_def.ml | 7 +++----
 4 files changed, 9 insertions(+), 17 deletions(-)

(limited to 'pretyping')

diff --git a/pretyping/classops.ml b/pretyping/classops.ml
index d21e1ba81..80fa10520 100755
--- a/pretyping/classops.ml
+++ b/pretyping/classops.ml
@@ -162,11 +162,8 @@ let (inClass,outClass) =
                     specification_function = (function x -> x) })
 
 let add_new_class (cl,s,stre,p) = 
-  let _ = 
-    Lib.add_anonymous_leaf (inClass ((cl,{cL_STR=s;cL_STRE=stre;cL_PARAM=p})))
-  in
-  ()
-    
+  Lib.add_anonymous_leaf (inClass ((cl,{cL_STR=s;cL_STRE=stre;cL_PARAM=p})))
+   
 let _ = 
   Summary.declare_summary "inh_graph"
     { Summary.freeze_function = freeze;
diff --git a/pretyping/pretyping.mli b/pretyping/pretyping.mli
index 9816beaa8..c4af6472d 100644
--- a/pretyping/pretyping.mli
+++ b/pretyping/pretyping.mli
@@ -49,8 +49,7 @@ val ise_resolve_type : bool -> 'a evar_map -> (int * constr) list ->
  * if we must coerce to a type *)
 val ise_resolve1 : bool -> 'a evar_map -> env -> rawconstr -> constr
 
-val ise_resolve_casted : 'a evar_map -> env -> 
-  constr -> rawconstr -> constr
+val ise_resolve_casted : 'a evar_map -> env -> constr -> rawconstr -> constr
 
 (* progmach.ml tries to type ill-typed terms: does not perform the conversion
  * test in application.
diff --git a/pretyping/recordops.ml b/pretyping/recordops.ml
index 590eff02b..dea95d0e0 100755
--- a/pretyping/recordops.ml
+++ b/pretyping/recordops.ml
@@ -44,9 +44,7 @@ let (inStruc,outStruc) =
                     specification_function = (function x -> x) })
 
 let add_new_struc (s,c,n,l) = 
-  let _ = 
-    Lib.add_anonymous_leaf (inStruc (s,{s_CONST=c;s_PARAM=n;s_PROJ=l})) in
-  ()
+  Lib.add_anonymous_leaf (inStruc (s,{s_CONST=c;s_PARAM=n;s_PROJ=l}))
 
 let struc_info s = List.assoc s !sTRUCS
 
@@ -83,9 +81,8 @@ let add_new_objdef (o,c,la,lp,l) =
   try 
     let _ = List.assoc o !oBJDEFS in ()
   with Not_found -> 
-    let _ = Lib.add_anonymous_leaf
-	      (inObjDef (o,{o_DEF=c;o_TABS=la;o_TPARAMS=lp;o_TCOMPS=l})) in
-    ()
+    Lib.add_anonymous_leaf
+      (inObjDef (o,{o_DEF=c;o_TABS=la;o_TPARAMS=lp;o_TCOMPS=l}))
 
 let ((inObjDef1:section_path -> obj),(outObjDef1:obj -> section_path)) =
   declare_object ("OBJDEF1",
diff --git a/pretyping/syntax_def.ml b/pretyping/syntax_def.ml
index 85f634405..6c5ef8c4f 100644
--- a/pretyping/syntax_def.ml
+++ b/pretyping/syntax_def.ml
@@ -31,13 +31,12 @@ let (in_syntax_constant, out_syntax_constant) =
     cache_function = cache_syntax_constant;
     load_function = (fun _ -> ());
     open_function = open_syntax_constant;
-    specification_function = (fun x -> x) } in
+    specification_function = (fun x -> x) } 
+  in
   declare_object ("SYNTAXCONSTANT", od)
 
 let declare_syntactic_definition id c =
-  let sp = add_leaf id CCI (in_syntax_constant c) in
-  add_syntax_constant id c;
-  Nametab.push (basename sp) sp
+  let _ = add_leaf id CCI (in_syntax_constant c) in ()
 
 let search_syntactic_definition id = Idmap.find id !syntax_table
 
-- 
cgit v1.2.3