From 0e1bf8990c7c3100f5c5ca50c99ead4f3858e76f Mon Sep 17 00:00:00 2001
From: Claudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Date: Tue, 9 Jun 2009 16:37:54 +0000
Subject: [PATCH] Temporary (and partially broken) patch for Ferruccio: I
 duplicate \Pi abstractions in let ... rec definitions in order to make the
 system infer the same names. However, it could be infer a -> in place of a
 \forall.

---
 .../components/cic_disambiguation/cicDisambiguate.ml         | 4 +++-
 helm/software/components/cic_unification/cicRefine.ml        | 1 +
 helm/software/components/grafite_parser/grafiteParser.ml     | 5 ++---
 helm/software/components/syntax_extensions/.depend           | 3 +++
 4 files changed, 9 insertions(+), 4 deletions(-)

diff --git a/helm/software/components/cic_disambiguation/cicDisambiguate.ml b/helm/software/components/cic_disambiguation/cicDisambiguate.ml
index 749f1434d..cf59ab553 100644
--- a/helm/software/components/cic_disambiguation/cicDisambiguate.ml
+++ b/helm/software/components/cic_disambiguation/cicDisambiguate.ml
@@ -352,9 +352,11 @@ let interpretate_term ~mk_choice ?(create_dummy_ids=false) ~context ~env ~uri
               in
               let cic_body =
                aux ~localize loc context' (add_binders `Lambda body) in
+              let typ =
+               match typ with Some typ -> typ | None-> CicNotationPt.Implicit in
               let cic_type =
                aux_option ~localize loc context (Some `Type)
-                (HExtlib.map_option (add_binders `Pi) typ) in
+                (Some (add_binders `Pi typ)) in
               let name =
                 match CicNotationUtil.cic_name_of_name name with
                 | Cic.Anonymous ->
diff --git a/helm/software/components/cic_unification/cicRefine.ml b/helm/software/components/cic_unification/cicRefine.ml
index b535b9ebe..56e010f7b 100644
--- a/helm/software/components/cic_unification/cicRefine.ml
+++ b/helm/software/components/cic_unification/cicRefine.ml
@@ -1967,6 +1967,7 @@ let typecheck metasenv uri obj ~localization_tbl =
  let ugraph = CicUniv.oblivion_ugraph in
  match obj with
     Cic.Constant (name,Some bo,ty,args,attrs) ->
+prerr_endline ("PRIMA: " ^ CicPp.ppobj obj);
      (* CSC: ugly code. Here I need to retrieve in advance the loc of bo
         since type_of_aux' destroys localization information (which are
         preserved by type_of_aux *)
diff --git a/helm/software/components/grafite_parser/grafiteParser.ml b/helm/software/components/grafite_parser/grafiteParser.ml
index 06a753f88..93cff174c 100644
--- a/helm/software/components/grafite_parser/grafiteParser.ml
+++ b/helm/software/components/grafite_parser/grafiteParser.ml
@@ -76,15 +76,14 @@ let mk_rec_corec ng ind_kind defs loc =
     `MutualDefinition to rememer this. *)
   let name,ty = 
     match defs with
-    | (params,(N.Ident (name, None), Some ty),_,_) :: _ ->
+    | (params,(N.Ident (name, None), ty),_,_) :: _ ->
+        let ty = match ty with Some ty -> ty | None -> N.Implicit in
         let ty =
          List.fold_right
           (fun var ty -> N.Binder (`Pi,var,ty)
           ) params ty
         in
          name,ty
-    | (_,(N.Ident (name, None), None),_,_) :: _ ->
-        name, N.Implicit
     | _ -> assert false 
   in
   let body = N.Ident (name,None) in
diff --git a/helm/software/components/syntax_extensions/.depend b/helm/software/components/syntax_extensions/.depend
index f3c6a8bd1..25e67131f 100644
--- a/helm/software/components/syntax_extensions/.depend
+++ b/helm/software/components/syntax_extensions/.depend
@@ -1,2 +1,5 @@
+utf8Macro.cmi: 
+utf8MacroTable.cmo: 
+utf8MacroTable.cmx: 
 utf8Macro.cmo: utf8MacroTable.cmo utf8Macro.cmi 
 utf8Macro.cmx: utf8MacroTable.cmx utf8Macro.cmi 
-- 
2.39.2