Added initial support for inversion principles in Matita NG.

[helm.git] / helm / software / components / content_pres / content2pres.ml

diff --git a/helm/software/components/content_pres/content2pres.ml b/helm/software/components/content_pres/content2pres.ml
index 63eec5e351a21dec9d50b7c2aedffc1ef580b433..c88f87535f71fe71aa6aac2e539060ad8cea7ae6 100644 (file)
--- a/helm/software/components/content_pres/content2pres.ml
+++ b/helm/software/components/content_pres/content2pres.ml
@@ -136,7 +136,8 @@ let rec justification ~for_rewriting_step ~ignore_atoms term2pres p =
       make_args_for_apply term2pres p.Con.proof_conclude.Con.conclude_args
     in
      [B.H([],
-       (if for_rewriting_step then (B.b_kw "exact") else (B.b_kw "by"))::
+     (*(if for_rewriting_step then (B.b_kw "exact") else (B.b_kw "by"))::*)
+       (B.b_kw "by")::
        B.b_space::
        B.Text([],"(")::pres_args@[B.Text([],")")])], None 
   else
@@ -927,17 +928,20 @@ let inductive2pres term2pres ind =
 
 let definition2pres ?recno term2pres d =
   let name = match d.Content.def_name with Some x -> x|_->assert false in
-  let rno = match recno with None -> assert false | Some x -> x in
+  let rno = match recno with None -> -1 (* cofix *) | Some x -> x in
   let ty = d.Content.def_type in
   let module P = CicNotationPt in
   let rec split_pi i t = 
     if i <= 1 then 
       match t with 
-      | P.Binder ((`Pi|`Forall),(var,_ as v),t) -> [v], var, t 
+      | P.Binder ((`Pi|`Forall),(var,_ as v),t) 
+      | P.AttributedTerm (_,P.Binder ((`Pi|`Forall),(var,_ as v),t)) -> 
+            [v], var, t 
       | _ -> assert false
     else
       match t with
-      | P.Binder ((`Pi|`Forall), var ,ty) ->
+      | P.Binder ((`Pi|`Forall), var ,ty) 
+      | P.AttributedTerm (_, P.Binder ((`Pi|`Forall), var ,ty)) ->
            let l, r, t = split_pi (i-1) ty in
            var :: l, r, t
       | _ -> assert false
@@ -955,8 +959,9 @@ let definition2pres ?recno term2pres d =
   in
   B.b_hv [] 
    [B.b_hv [] 
-    ([ B.b_space; B.b_text [] name ] @ params @
-       [B.b_kw "on" ; B.b_space; term2pres rec_param ; B.b_space;
+    ([ B.b_space; B.b_text [] name; B.b_space ] @ params @
+    (if rno <> -1 then [B.b_kw "on" ; B.b_space; term2pres rec_param ] else [])
+    @[ B.b_space;
        B.b_text [] ":"; B.b_space; term2pres ty]); 
    B.b_text [] ":=";
    B.b_h [] [B.b_space;term2pres body] ]