sort CProp added

diff --git a/helm/Makefile b/helm/Makefile
index 0b925d51504ec6fd25ef2a2f91da8aa2e98dda40..721a8962121a6593e450a009b785fad81e5ea0a8 100644 (file)
--- a/helm/Makefile
+++ b/helm/Makefile
@@ -1,5 +1,4 @@
-DIRS = ocaml gTopLevel searchEngine mathql_test
-# hbugs
+DIRS = ocaml hbugs gTopLevel searchEngine mathql_test
 
 DIRS_BYTE = $(patsubst %,%.byte,$(DIRS))
 DIRS_OPT = $(patsubst %,%.opt,$(DIRS))

diff --git a/helm/gTopLevel/.depend b/helm/gTopLevel/.depend
index 6da67a4a543564085fbe41e7a48949017e375064..e7f7c2d1dd67f5b5dbc04583f5a211ddc9002da6 100644 (file)
--- a/helm/gTopLevel/.depend
+++ b/helm/gTopLevel/.depend
@@ -1,6 +1,7 @@
 termEditor.cmi: disambiguate.cmi 
 texTermEditor.cmi: disambiguate.cmi 
 invokeTactics.cmi: termEditor.cmi termViewer.cmi 
+hbugs.cmi: invokeTactics.cmi 
 proofEngine.cmo: proofEngine.cmi 
 proofEngine.cmx: proofEngine.cmi 
 logicalOperations.cmo: proofEngine.cmi logicalOperations.cmi 
@@ -19,7 +20,9 @@ invokeTactics.cmo: logicalOperations.cmi proofEngine.cmi termEditor.cmi \
     termViewer.cmi invokeTactics.cmi 
 invokeTactics.cmx: logicalOperations.cmx proofEngine.cmx termEditor.cmx \
     termViewer.cmx invokeTactics.cmi 
-gTopLevel.cmo: invokeTactics.cmi logicalOperations.cmi proofEngine.cmi \
-    termEditor.cmi termViewer.cmi texTermEditor.cmi 
-gTopLevel.cmx: invokeTactics.cmx logicalOperations.cmx proofEngine.cmx \
-    termEditor.cmx termViewer.cmx texTermEditor.cmx 
+hbugs.cmo: invokeTactics.cmi proofEngine.cmi hbugs.cmi 
+hbugs.cmx: invokeTactics.cmx proofEngine.cmx hbugs.cmi 
+gTopLevel.cmo: hbugs.cmi invokeTactics.cmi logicalOperations.cmi \
+    proofEngine.cmi termEditor.cmi termViewer.cmi texTermEditor.cmi 
+gTopLevel.cmx: hbugs.cmx invokeTactics.cmx logicalOperations.cmx \
+    proofEngine.cmx termEditor.cmx termViewer.cmx texTermEditor.cmx 

diff --git a/helm/gTopLevel/Makefile b/helm/gTopLevel/Makefile
index 9c9aaea62093ff46d45db89e6b32c21e426830ac..7ce96c052cf277508b4e0b9c1912d9aaaa6fb89f 100644 (file)
--- a/helm/gTopLevel/Makefile
+++ b/helm/gTopLevel/Makefile
@@ -2,7 +2,7 @@ BIN_DIR = /usr/local/bin
 REQUIRES = lablgtkmathview helm-cic_textual_parser helm-tex_cic_textual_parser \
            helm-cic_proof_checking helm-xml gdome2-xslt helm-cic_unification \
            helm-mathql helm-mathql_interpreter helm-mathql_generator \
-                helm-tactics threads hbugs-client mathml-editor \
+          helm-tactics threads hbugs-client mathml-editor \
            helm-cic_transformations
 PREDICATES = "gnome,init,glade"
 OCAMLOPTIONS = -package "$(REQUIRES)" -predicates "$(PREDICATES)" -pp camlp4o
@@ -77,11 +77,3 @@ uninstall:
 ifneq ($(MAKECMDGOALS), depend)
    include .depend   
 endif
-
-
-
-
-
-
-
-

diff --git a/helm/gTopLevel/gTopLevel.ml b/helm/gTopLevel/gTopLevel.ml
index 88d819fded0abd67afdc1a8f4a8dce14af9f1835..8aec9d350d49f55b88a0235077397b796076efd1 100644 (file)
--- a/helm/gTopLevel/gTopLevel.ml
+++ b/helm/gTopLevel/gTopLevel.ml
@@ -672,7 +672,7 @@ module InvokeTacticsCallbacks =
  end
 ;;
 module InvokeTactics' = InvokeTactics.Make (InvokeTacticsCallbacks);;
-
+(*
 (* Just to initialize the Hbugs module *)
 module Ignore = Hbugs.Initialize (InvokeTactics');;
 Hbugs.set_describe_hint_callback (fun hint ->
@@ -682,7 +682,7 @@ Hbugs.set_describe_hint_callback (fun hint ->
       check_window outputhtml [term]
   | _ -> ())
 ;;
-
+*)
 let dummy_uri = "/dummy.con"
 
   (** load an unfinished proof from filesystem *)

diff --git a/helm/gTopLevel/termViewer.ml b/helm/gTopLevel/termViewer.ml
index b782237d0379f24d06f39d56e71940c0f04cb45b..e105d5f0ea32ef9a3df3b50b66a1e6bd80872628 100644 (file)
--- a/helm/gTopLevel/termViewer.ml
+++ b/helm/gTopLevel/termViewer.ml
@@ -113,8 +113,10 @@ class sequent_viewer obj =
     ApplyStylesheets.mml_of_cic_sequent metasenv sequent
    in
     self#load_doc ~dom:sequent_mml ;
+(*
 Misc.domImpl#saveDocumentToFile ~name:"/tmp/pippo" ~doc:sequent_mml () ;
-    current_infos <-
+*)
+     current_infos <-
      Some (ids_to_terms,ids_to_father_ids,ids_to_hypotheses)
  end
 ;;

diff --git a/helm/ocaml/cic/cic.ml b/helm/ocaml/cic/cic.ml
index 6d58e6164336dbb8fecf6a5e8007f5ef77b31bae..cb2af219b89daaa904577ff83c93ebb8e1c98086 100644 (file)
--- a/helm/ocaml/cic/cic.ml
+++ b/helm/ocaml/cic/cic.ml
@@ -51,6 +51,7 @@ and sort =
    Prop
  | Set
  | Type
+ | CProp
 and name =
    Name of string
  | Anonymous

diff --git a/helm/ocaml/cic_omdoc/cic2acic.ml b/helm/ocaml/cic_omdoc/cic2acic.ml
index d934e83bfa4443581c161f53ef5a5d1f80f9d79e..aa0183dad1514c05367818598267012215dcf16b 100644 (file)
--- a/helm/ocaml/cic_omdoc/cic2acic.ml
+++ b/helm/ocaml/cic_omdoc/cic2acic.ml
@@ -100,10 +100,11 @@ let acic_of_cic_context' seed ids_to_terms ids_to_father_ids ids_to_inner_sorts
       (*CSC: computed again and again.                               *)
       let string_of_sort t =
        match CicReduction.whd context t with 
-          C.Sort C.Prop -> "Prop"
-        | C.Sort C.Set  -> "Set"
-        | C.Sort C.Type -> "Type"
-        | _ -> assert false
+          C.Sort C.Prop  -> "Prop"
+        | C.Sort C.Set   -> "Set"
+        | C.Sort C.Type  -> "Type"
+       | C.Sort C.CProp -> "CProp"
+        | _              -> assert false
       in
        let ainnertypes,innertype,innersort,expected_available =
 (*CSC: Here we need the algorithm for Coscoy's double type-inference  *)

diff --git a/helm/ocaml/cic_omdoc/doubleTypeInference.ml b/helm/ocaml/cic_omdoc/doubleTypeInference.ml
index 03227ef9b75df7af38c9bcac6db2f8e9d201d737..f51c00c74dc3271d861a2d7ab0b9a65313b75baf 100644 (file)
--- a/helm/ocaml/cic_omdoc/doubleTypeInference.ml
+++ b/helm/ocaml/cic_omdoc/doubleTypeInference.ml
@@ -647,7 +647,7 @@ let rec type_of_aux' subterms_to_types metasenv context t expectedty =
    let t2' = CicReduction.whd ((Some (name,C.Decl s))::context) t2 in
    match (t1', t2') with
       (C.Sort s1, C.Sort s2)
-        when (s2 = C.Prop or s2 = C.Set) -> (* different from Coq manual!!! *)
+        when (s2 = C.Prop or s2 = C.Set or s2 = C.CProp) -> (* different from Coq manual!!! *)
          C.Sort s2
     | (C.Sort s1, C.Sort s2) -> C.Sort C.Type (*CSC manca la gestione degli universi!!! *)
     | (_,_) ->

diff --git a/helm/ocaml/cic_proof_checking/cicPp.ml b/helm/ocaml/cic_proof_checking/cicPp.ml
index 11ed4418c67f8f4eae0f0244397306f45c62354e..a8d9eaa0bdd87e4ef67c60611e4c8e314b0f53cd 100644 (file)
--- a/helm/ocaml/cic_proof_checking/cicPp.ml
+++ b/helm/ocaml/cic_proof_checking/cicPp.ml
@@ -83,9 +83,10 @@ let rec pp t l =
         "]"
     | C.Sort s ->
        (match s with
-           C.Prop -> "Prop"
-         | C.Set  -> "Set"
-         | C.Type -> "Type"
+           C.Prop  -> "Prop"
+         | C.Set   -> "Set"
+         | C.Type  -> "Type"
+        | C.CProp -> "CProp" 
        )
     | C.Implicit -> "?"
     | C.Prod (b,s,t) ->

diff --git a/helm/ocaml/cic_proof_checking/cicTypeChecker.ml b/helm/ocaml/cic_proof_checking/cicTypeChecker.ml
index 62dc951aaa54deb58cc3fe0dc36dfa5e142a4fac..7521f0f90b0456ca0ec8c0bf4c4e9a2d18922c25 100644 (file)
--- a/helm/ocaml/cic_proof_checking/cicTypeChecker.ml
+++ b/helm/ocaml/cic_proof_checking/cicTypeChecker.ml
@@ -1185,6 +1185,7 @@ and check_allowed_sort_elimination context uri i need_dummy ind arity1 arity2 =
         (C.Appl [CicSubstitution.lift 1 ind ; C.Rel 1]) de1 de2
    | (C.Sort C.Prop, C.Sort C.Prop) when need_dummy -> true
    | (C.Sort C.Prop, C.Sort C.Set)
+   | (C.Sort C.Prop, C.Sort C.CProp)
    | (C.Sort C.Prop, C.Sort C.Type) when need_dummy ->
 (*CSC: WRONG. MISSING CONDITIONS ON THE ARGUMENTS OF THE CONSTRUTOR *)
        (match CicEnvironment.get_obj uri with
@@ -1198,8 +1199,13 @@ and check_allowed_sort_elimination context uri i need_dummy ind arity1 arity2 =
               (WrongUriToMutualInductiveDefinitions (U.string_of_uri uri)))
        )
    | (C.Sort C.Set, C.Sort C.Prop) when need_dummy -> true
+   | (C.Sort C.CProp, C.Sort C.Prop) when need_dummy -> true
    | (C.Sort C.Set, C.Sort C.Set) when need_dummy -> true
-   | (C.Sort C.Set, C.Sort C.Type) when need_dummy ->
+   | (C.Sort C.Set, C.Sort C.CProp) when need_dummy -> true
+   | (C.Sort C.CProp, C.Sort C.Set) when need_dummy -> true
+   | (C.Sort C.CProp, C.Sort C.CProp) when need_dummy -> true
+   | ((C.Sort C.Set, C.Sort C.Type) | (C.Sort C.CProp, C.Sort C.Type))
+      when need_dummy ->
        (match CicEnvironment.get_obj uri with
            C.InductiveDefinition (itl,_,paramsno) ->
             let tys =
@@ -1220,7 +1226,7 @@ and check_allowed_sort_elimination context uri i need_dummy ind arity1 arity2 =
         res &&
         (match CicReduction.whd ((Some (name,(C.Decl so)))::context) ta with
             C.Sort C.Prop -> true
-          | C.Sort C.Set ->
+          | (C.Sort C.Set | C.Sort C.CProp) ->
              (match CicEnvironment.get_obj uri with
                  C.InductiveDefinition (itl,_,_) ->
                   let (_,_,_,cl) = List.nth itl i in
@@ -1233,13 +1239,15 @@ and check_allowed_sort_elimination context uri i need_dummy ind arity1 arity2 =
              )
           | _ -> false
         )
-   | (C.Sort C.Set, C.Prod (name,so,ta)) when not need_dummy ->
+   | ((C.Sort C.Set, C.Prod (name,so,ta)) | (C.Sort C.CProp, C.Prod (name,so,ta)))
+      when not need_dummy ->
        let res = CicReduction.are_convertible context so ind
        in
         res &&
         (match CicReduction.whd ((Some (name,(C.Decl so)))::context) ta with
             C.Sort C.Prop
           | C.Sort C.Set  -> true
+         | C.Sort C.CProp -> true
           | C.Sort C.Type ->
              (match CicEnvironment.get_obj uri with
                  C.InductiveDefinition (itl,_,paramsno) ->
@@ -1647,7 +1655,7 @@ in if not res then prerr_endline ("#### " ^ CicPp.ppterm (type_of_aux context p)
    let t2' = CicReduction.whd ((Some (name,C.Decl s))::context) t2 in
    match (t1', t2') with
       (C.Sort s1, C.Sort s2)
-        when (s2 = C.Prop or s2 = C.Set) -> (* different from Coq manual!!! *)
+        when (s2 = C.Prop or s2 = C.Set or s2 = C.CProp) -> (* different from Coq manual!!! *)
          C.Sort s2
     | (C.Sort s1, C.Sort s2) -> C.Sort C.Type (*CSC manca la gestione degli universi!!! *)
     | (_,_) ->
@@ -1728,7 +1736,7 @@ and is_small context paramsno c =
       C.Prod (n,so,de) ->
        (*CSC: [] is an empty metasenv. Is it correct? *)
        let s = type_of_aux' [] context so in
-        (s = C.Sort C.Prop || s = C.Sort C.Set) &&
+        (s = C.Sort C.Prop || s = C.Sort C.Set || s = C.Sort C.CProp) &&
         is_small_aux ((Some (n,(C.Decl so)))::context) de
     | _ -> true (*CSC: we trust the type-checker *)
  in

diff --git a/helm/ocaml/cic_textual_parser/cicTextualLexer.mll b/helm/ocaml/cic_textual_parser/cicTextualLexer.mll
index 6db492ee1745319fe06cb400f4860adfc6066112..613645bc489ed28b2fa9ff82b27af0ad76454f99 100644 (file)
--- a/helm/ocaml/cic_textual_parser/cicTextualLexer.mll
+++ b/helm/ocaml/cic_textual_parser/cicTextualLexer.mll
@@ -74,6 +74,7 @@ rule token =
   | "Set"       { SET }
   | "Prop"      { PROP }
   | "Type"      { TYPE }
+  | "CProp"     { CPROP }
   | ident       { ID (L.lexeme lexbuf) }
   | conuri      { CONURI (U.uri_of_string ("cic:" ^ L.lexeme lexbuf)) }
   | varuri      { VARURI (U.uri_of_string ("cic:" ^ L.lexeme lexbuf)) }

diff --git a/helm/ocaml/cic_textual_parser/cicTextualParser.mly b/helm/ocaml/cic_textual_parser/cicTextualParser.mly
index 08d85a595a2b03c358f07586ffdd4eb86ab5c30a..84e0f0ee50bcc4f90808fac592323016252e8863 100644 (file)
--- a/helm/ocaml/cic_textual_parser/cicTextualParser.mly
+++ b/helm/ocaml/cic_textual_parser/cicTextualParser.mly
@@ -155,7 +155,7 @@
 %token <UriManager.uri> VARURI
 %token <UriManager.uri * int> INDTYURI
 %token <UriManager.uri * int * int> INDCONURI
-%token LPAREN RPAREN PROD LAMBDA COLON DOT SET PROP TYPE CAST IMPLICIT NONE
+%token LPAREN RPAREN PROD LAMBDA COLON DOT SET PROP TYPE CPROP CAST IMPLICIT NONE
 %token LETIN FIX COFIX SEMICOLON LCURLY RCURLY CASE ARROW LBRACKET RBRACKET EOF
 %right ARROW
 %start main
@@ -286,9 +286,10 @@ expr2:
     }
  | IMPLICIT
     { mk_implicit () }
- | SET  { [], function _ -> Sort Set }
- | PROP { [], function _ -> Sort Prop }
- | TYPE { [], function _ -> Sort Type }
+ | SET   { [], function _ -> Sort Set }
+ | PROP  { [], function _ -> Sort Prop }
+ | TYPE  { [], function _ -> Sort Type }
+ | CPROP { [], function _ -> Sort CProp }
  | LPAREN expr CAST expr RPAREN
     { let dom1,mk_expr1 = $2 in
       let dom2,mk_expr2 = $4 in

diff --git a/helm/ocaml/cic_transformations/cic2Xml.ml b/helm/ocaml/cic_transformations/cic2Xml.ml
index d945cc82f63d54b2e931424c625dacd9707ba383..7594ffef1a5c4f57d00ed4631179960b2d44115b 100644 (file)
--- a/helm/ocaml/cic_transformations/cic2Xml.ml
+++ b/helm/ocaml/cic_transformations/cic2Xml.ml
@@ -72,9 +72,10 @@ let print_term ~ids_to_inner_sorts =
      | C.ASort (id,s) ->
         let string_of_sort =
          function
-            C.Prop -> "Prop"
-          | C.Set  -> "Set"
-          | C.Type -> "Type"
+            C.Prop  -> "Prop"
+          | C.Set   -> "Set"
+          | C.Type  -> "Type"
+         | C.CProp -> "CProp"
         in
          X.xml_empty "SORT" [None,"value",(string_of_sort s) ; None,"id",id]
      | C.AImplicit _ -> raise NotImplemented

diff --git a/helm/ocaml/cic_transformations/content_expressions.ml b/helm/ocaml/cic_transformations/content_expressions.ml
index 2ff989da184439ef060b5344e4dcbbdbf501a89a..b913bf0de63e6ba2d28341b23188975d713b2bf6 100644 (file)
--- a/helm/ocaml/cic_transformations/content_expressions.ml
+++ b/helm/ocaml/cic_transformations/content_expressions.ml
@@ -303,9 +303,10 @@ Hashtbl.add symbol_table "cic:/Coq/Reals/Rdefinitions/Rdiv.con"
  
 let string_of_sort =
   function 
-    Cic.Prop -> "Prop"
-  | Cic.Set  -> "Set"
-  | Cic.Type -> "Type"
+    Cic.Prop  -> "Prop"
+  | Cic.Set   -> "Set"
+  | Cic.Type  -> "Type"
+  | Cic.CProp -> "Type"
 ;;
 
 let get_constructors uri i =

diff --git a/helm/ocaml/cic_unification/cicRefine.ml b/helm/ocaml/cic_unification/cicRefine.ml
index 881c72bfd516852218105dc56ce71653219ce4d8..ba79ce92232f4cce5866786b6d6b8ea4e4b3133e 100644 (file)
--- a/helm/ocaml/cic_unification/cicRefine.ml
+++ b/helm/ocaml/cic_unification/cicRefine.ml
@@ -290,7 +290,7 @@ and type_of_aux' metasenv context t =
     let t2'' = CicReduction.whd ((Some (name,C.Decl s))::context) t2' in
     match (t1'', t2'') with
        (C.Sort s1, C.Sort s2)
-         when (s2 = C.Prop or s2 = C.Set) -> (* different from Coq manual!!! *)
+         when (s2 = C.Prop or s2 = C.Set or s2 = C.CProp) -> (* different from Coq manual!!! *)
           C.Sort s2,subst',metasenv'
      | (C.Sort s1, C.Sort s2) ->
          (*CSC manca la gestione degli universi!!! *)

diff --git a/helm/ocaml/mathql_generator/cGSearchPattern.ml b/helm/ocaml/mathql_generator/cGSearchPattern.ml
index 77f3b488c6e896a7285e3ef2a0c73e2f415f87d9..a56d65959448421f872acc554e00edb194359ab8 100644 (file)
--- a/helm/ocaml/mathql_generator/cGSearchPattern.ml
+++ b/helm/ocaml/mathql_generator/cGSearchPattern.ml
@@ -96,6 +96,7 @@ let get_constraints term =
                 Cic.Prop -> T.Prop
               | Cic.Set -> T.Set
               | Cic.Type -> T.Type
+             | Cic.CProp -> T.CProp
             in
             [],[],[!!kind,s']
          | _ -> [],[],[])

diff --git a/helm/ocaml/mathql_generator/mQGTypes.ml b/helm/ocaml/mathql_generator/mQGTypes.ml
index 2dacfe14c5d045690a8f33f12b0bd1ae678546e6..a210aa68f355e1b9bc95744255a9f9440da52716 100644 (file)
--- a/helm/ocaml/mathql_generator/mQGTypes.ml
+++ b/helm/ocaml/mathql_generator/mQGTypes.ml
@@ -39,6 +39,7 @@ type depth = int
 type sort = Set
           | Prop
           | Type
+         | CProp
  
 type spec = MustObj  of uri list * position list * depth list
           | MustSort of sort list * position list * depth list

diff --git a/helm/ocaml/mathql_generator/mQGUtil.ml b/helm/ocaml/mathql_generator/mQGUtil.ml
index 36dd0653c67f83256c4276dc8b8540798739fabe..e30742649ab5f50bfdc986855c0893054a5847e3 100644 (file)
--- a/helm/ocaml/mathql_generator/mQGUtil.ml
+++ b/helm/ocaml/mathql_generator/mQGUtil.ml
@@ -40,9 +40,10 @@ let string_of_position p =
       | T.InBody         -> ns ^ "InBody"
       
 let string_of_sort = function
-   | T.Set  -> "Set"
-   | T.Prop -> "Prop"
-   | T.Type -> "Type"
+   | T.Set   -> "Set"
+   | T.Prop  -> "Prop"
+   | T.Type  -> "Type"
+   | T.CProp -> "CProp"
 
 let string_of_depth = string_of_int
 
@@ -54,9 +55,10 @@ let mathql_of_position = function
    | T.InBody         -> "$IB"
       
 let mathql_of_sort = function
-   | T.Set  -> "$SET"
-   | T.Prop -> "$PROP"
-   | T.Type -> "$TYPE"
+   | T.Set   -> "$SET"
+   | T.Prop  -> "$PROP"
+   | T.Type  -> "$TYPE"
+   | T.CProp -> "$CPROP"
 
 let mathql_of_depth = string_of_int
 
@@ -92,9 +94,10 @@ let position_of_mathql = function
    | _     -> raise Parsing.Parse_error 
 
 let sort_of_mathql = function
-   | "$SET"  -> T.Set 
-   | "$PROP" -> T.Prop
-   | "$TYPE" -> T.Type
+   | "$SET"   -> T.Set 
+   | "$PROP"  -> T.Prop
+   | "$TYPE"  -> T.Type
+   | "$CPROP" -> T.CProp
    | _       -> raise Parsing.Parse_error 
 
 let depth_of_mathql s =
@@ -120,9 +123,10 @@ let text_of_depth pos no_depth_text = match pos with
    | _                        -> no_depth_text
 
 let text_of_sort = function
-   | T.Set  -> "Set"
-   | T.Prop -> "Prop"
-   | T.Type -> "Type"
+   | T.Set   -> "Set"
+   | T.Prop  -> "Prop"
+   | T.Type  -> "Type"
+   | T.CProp -> "CProp"
 
 let is_main_position = function
    | `MainHypothesis _

diff --git a/helm/ocaml/mathql_interpreter/mQueryTLexer.mll b/helm/ocaml/mathql_interpreter/mQueryTLexer.mll
index abccb46264d2053927ded64beec8bb60169eefd5..ca51751f09a7ac9f50d340da4adce6d683823a30 100644 (file)
--- a/helm/ocaml/mathql_interpreter/mQueryTLexer.mll
+++ b/helm/ocaml/mathql_interpreter/mQueryTLexer.mll
@@ -123,6 +123,7 @@ and result_token = parse
    | SPC         { result_token lexbuf }
    | "(*"        { comm_token lexbuf; result_token lexbuf }
    | '"'         { STR (qstr string_token lexbuf) }
+   | '/'         { out "SL"; SL }
    | '{'         { LC }
    | '}'         { RC }
    | ','         { CM }

diff --git a/helm/ocaml/tactics/equalityTactics.ml b/helm/ocaml/tactics/equalityTactics.ml
index 1c2a7d37fb1a83fc9e15cfc9ec989088a9af57f5..a663282207c6057ae94cf4fdf4e7360bc74ba58f 100644 (file)
--- a/helm/ocaml/tactics/equalityTactics.ml
+++ b/helm/ocaml/tactics/equalityTactics.ml
@@ -164,6 +164,7 @@ let replace_tac ~what ~with_what ~status:((proof, goal) as status) =
          match CicTypeChecker.type_of_aux' metasenv context wty with
             C.Sort C.Set -> "cic:/Coq/Init/Logic/eq.ind"
           | C.Sort C.Type
+         | C.Sort C.CProp
           | C.Sort C.Prop -> "cic:/Coq/Init/Logic_Type/eqT.ind"
           | _ -> assert false
         in

diff --git a/helm/ocaml/tactics/primitiveTactics.ml b/helm/ocaml/tactics/primitiveTactics.ml
index 8dfdd66c494cb2659ce11294dfeb4490928d8442..b060e009e067f012d8e4dd7e1ee469e7fdfb93c9 100644 (file)
--- a/helm/ocaml/tactics/primitiveTactics.ml
+++ b/helm/ocaml/tactics/primitiveTactics.ml
@@ -420,6 +420,7 @@ let elim_tac ~term ~status:(proof, goal) =
       match T.type_of_aux' metasenv context ty with
          C.Sort C.Prop -> "_ind"
        | C.Sort C.Set  -> "_rec"
+       | C.Sort C.CProp -> "_rec"
        | C.Sort C.Type -> "_rect"
        | _ -> assert false
      in

diff --git a/helm/ocaml/tactics/proofEngineHelpers.ml b/helm/ocaml/tactics/proofEngineHelpers.ml
index ac5850ca285c07a19f9d6e07e27ffbf442488e44..79304211deb0e8a69f3f1072a8657dc2a33510fa 100644 (file)
--- a/helm/ocaml/tactics/proofEngineHelpers.ml
+++ b/helm/ocaml/tactics/proofEngineHelpers.ml
@@ -36,6 +36,7 @@ let mk_fresh_name context name ~typ =
        (try
          (match CicTypeChecker.type_of_aux' [] context typ with
              C.Sort C.Prop -> "H"
+          | C.Sort C.CProp -> "H"
            | C.Sort C.Set -> "x"
            | _ -> "H"
          )

diff --git a/helm/ocaml/tex_cic_textual_parser/texCicTextualLexer.mll b/helm/ocaml/tex_cic_textual_parser/texCicTextualLexer.mll
index f6eda1ac8f8f26cd4a53a16e7c187ead58769e29..5ab17fa80ce5e5879bf4a33320b3acc5b36802cc 100644 (file)
--- a/helm/ocaml/tex_cic_textual_parser/texCicTextualLexer.mll
+++ b/helm/ocaml/tex_cic_textual_parser/texCicTextualLexer.mll
@@ -81,6 +81,7 @@ rule token =
   | "\\Set"     { SET }
   | "\\Prop"    { PROP }
   | "\\Type"    { TYPE }
+  | "\\CProp"   { CPROP }
   | ident       { ID (unquote (L.lexeme lexbuf)) }
   | conuri      { CONURI
                    (U.uri_of_string ("cic:" ^ (unquote (L.lexeme lexbuf)))) }

diff --git a/helm/ocaml/tex_cic_textual_parser/texCicTextualParser.mly b/helm/ocaml/tex_cic_textual_parser/texCicTextualParser.mly
index 500565823d20a328166fd06dda7e2222d4860777..f6f557947a0598509c1ce9c45f66fc0f79b99009 100644 (file)
--- a/helm/ocaml/tex_cic_textual_parser/texCicTextualParser.mly
+++ b/helm/ocaml/tex_cic_textual_parser/texCicTextualParser.mly
@@ -156,7 +156,7 @@
 %token <UriManager.uri> VARURI
 %token <UriManager.uri * int> INDTYURI
 %token <UriManager.uri * int * int> INDCONURI
-%token LPAREN RPAREN PROD LAMBDA COLON DOT SET PROP TYPE CAST IMPLICIT NONE
+%token LPAREN RPAREN PROD LAMBDA COLON DOT SET PROP TYPE CPROP CAST IMPLICIT NONE
 %token LETIN FIX COFIX SEMICOLON LCURLY RCURLY CASE ARROW LBRACKET RBRACKET EOF
 %token DOLLAR
 %token RPLUS RMINUS RTIMES RDIV
@@ -473,9 +473,10 @@ expr2:
     }
  | IMPLICIT
     { mk_implicit () }
- | SET  { [], function _ -> Sort Set }
- | PROP { [], function _ -> Sort Prop }
- | TYPE { [], function _ -> Sort Type }
+ | SET   { [], function _ -> Sort Set }
+ | PROP  { [], function _ -> Sort Prop }
+ | TYPE  { [], function _ -> Sort Type }
+ | CPROP { [], function _ -> Sort CProp }
  | LPAREN expr CAST expr RPAREN
     { let dom1,mk_expr1 = $2 in
       let dom2,mk_expr2 = $4 in