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.

diff --git a/helm/software/components/cic_disambiguation/cicDisambiguate.ml b/helm/software/components/cic_disambiguation/cicDisambiguate.ml
index 749f1434d2f82a34337fdd9d245d2e377672a084..cf59ab553c33efc202208ea7d0cea86f7734aa74 100644 (file)
--- 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 b535b9ebe987677505d7d9b40a2c59731a4c2606..56e010f7bad2a48f8a10793cb1dc5b4052ac185e 100644 (file)
--- 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 06a753f88d42f4b2e4475f06883b56e86e4ee08e..93cff174c4fb26e1c99334a761aef12e1b7aba14 100644 (file)
--- 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 f3c6a8bd17a7351e99ce8e59905fda76a37cbf08..25e67131fca0487c4390d310d8307722b5058067 100644 (file)
--- 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