attributes support

diff --git a/helm/ocaml/cic_proof_checking/cicReductionMachine.ml b/helm/ocaml/cic_proof_checking/cicReductionMachine.ml
index e456a1731b226d3e66cd4718a12aeb19dab0f165..0610504c4faeaa389c8c65e6ea804acb1542d6fe 100644 (file)
--- a/helm/ocaml/cic_proof_checking/cicReductionMachine.ml
+++ b/helm/ocaml/cic_proof_checking/cicReductionMachine.ml
@@ -38,7 +38,7 @@ let debug t env s =
  let rec debug_aux t i =
   let module C = Cic in
   let module U = UriManager in
-   CicPp.ppobj (C.Variable ("DEBUG", None, t, [])) ^ "\n" ^ i
+   CicPp.ppobj (C.Variable ("DEBUG", None, t, [], [])) ^ "\n" ^ i
  in
   if !fdebug = 0 then
    prerr_endline (s ^ "\n" ^ List.fold_right debug_aux (t::env) "")
@@ -358,7 +358,7 @@ prerr_endline ("%%%%%UWVAR " ^ String.concat " ; " (List.map (function (uri,t) -
            in
            (match o with
                C.Constant _ -> raise ReferenceToConstant
-             | C.Variable (_,_,_,params) -> params
+             | C.Variable (_,_,_,params,_) -> params
              | C.CurrentProof _ -> raise ReferenceToCurrentProof
              | C.InductiveDefinition _ -> raise ReferenceToInductiveDefinition
            )
@@ -389,9 +389,9 @@ prerr_endline ("%%%%%UWVAR " ^ String.concat " ; " (List.map (function (uri,t) -
              CicEnvironment.get_cooked_obj CicUniv.empty_ugraph uri
            in
            (match o with
-               C.Constant (_,_,_,params) -> params
+               C.Constant (_,_,_,params,_) -> params
              | C.Variable _ -> raise ReferenceToVariable
-             | C.CurrentProof (_,_,_,_,params) -> params
+             | C.CurrentProof (_,_,_,_,params,_) -> params
              | C.InductiveDefinition _ -> raise ReferenceToInductiveDefinition
            )
           in
@@ -408,7 +408,7 @@ prerr_endline ("%%%%%UWVAR " ^ String.concat " ; " (List.map (function (uri,t) -
                C.Constant _ -> raise ReferenceToConstant
              | C.Variable _ -> raise ReferenceToVariable
              | C.CurrentProof _ -> raise ReferenceToCurrentProof
-             | C.InductiveDefinition (_,params,_) -> params
+             | C.InductiveDefinition (_,params,_,_) -> params
            )
           in
            let exp_named_subst' =
@@ -424,7 +424,7 @@ prerr_endline ("%%%%%UWVAR " ^ String.concat " ; " (List.map (function (uri,t) -
                C.Constant _ -> raise ReferenceToConstant
              | C.Variable _ -> raise ReferenceToVariable
              | C.CurrentProof _ -> raise ReferenceToCurrentProof
-             | C.InductiveDefinition (_,params,_) -> params
+             | C.InductiveDefinition (_,params,_,_) -> params
            )
           in
            let exp_named_subst' =
@@ -549,11 +549,11 @@ if List.mem uri params then prerr_endline "---- OK2" ;
               C.Constant _ -> raise ReferenceToConstant
             | C.CurrentProof _ -> raise ReferenceToCurrentProof
             | C.InductiveDefinition _ -> raise ReferenceToInductiveDefinition
-            | C.Variable (_,None,_,_) ->
+            | C.Variable (_,None,_,_,_) ->
                let t' = unwind k e ens t in
                 if s = [] then t' else
                  C.Appl (t'::(RS.from_stack_list ~unwind s))
-            | C.Variable (_,Some body,_,_) ->
+            | C.Variable (_,Some body,_,_,_) ->
                let ens' = push_exp_named_subst k e ens exp_named_subst in
                 reduce (0, [], ens', body, s)
           )
@@ -604,15 +604,15 @@ if List.mem uri params then prerr_endline "---- OK2" ;
           CicEnvironment.get_cooked_obj CicUniv.empty_ugraph uri
         in
          match o with
-            C.Constant (_,Some body,_,_) ->
+            C.Constant (_,Some body,_,_,_) ->
              let ens' = push_exp_named_subst k e ens exp_named_subst in
               (* constants are closed *)
               reduce (0, [], ens', body, s) 
-          | C.Constant (_,None,_,_) ->
+          | C.Constant (_,None,_,_,_) ->
              let t' = unwind k e ens t in
               if s = [] then t' else C.Appl (t'::(RS.from_stack_list ~unwind s))
           | C.Variable _ -> raise ReferenceToVariable
-          | C.CurrentProof (_,_,body,_,_) ->
+          | C.CurrentProof (_,_,body,_,_,_) ->
              let ens' = push_exp_named_subst k e ens exp_named_subst in
               (* constants are closed *)
               reduce (0, [], ens', body, s)
@@ -662,7 +662,7 @@ if List.mem uri params then prerr_endline "---- OK2" ;
                  CicEnvironment.get_cooked_obj CicUniv.empty_ugraph mutind 
                in
                  match o with
-                      C.InductiveDefinition (tl,ingredients,r) ->
+                      C.InductiveDefinition (tl,ingredients,r,_) ->
                        let (_,_,arity,_) = List.nth tl i in
                          (arity,r)
                     | _ -> raise WrongUriToInductiveDefinition

diff --git a/helm/ocaml/cic_proof_checking/cicReductionNaif.ml b/helm/ocaml/cic_proof_checking/cicReductionNaif.ml
index 4df3a5bd4bb5d1384ec3dceb1489bcad2bccc4e6..04067ccbfdfbb27663920b6ca3c2e46c9309f3b5 100644 (file)
--- a/helm/ocaml/cic_proof_checking/cicReductionNaif.ml
+++ b/helm/ocaml/cic_proof_checking/cicReductionNaif.ml
@@ -31,7 +31,7 @@ let debug t env s =
  let rec debug_aux t i =
   let module C = Cic in
   let module U = UriManager in
-   CicPp.ppobj (C.Variable ("DEBUG", None, t, [])) ^ "\n" ^ i
+   CicPp.ppobj (C.Variable ("DEBUG", None, t, [], [])) ^ "\n" ^ i
  in
   if !fdebug = 0 then
    prerr_endline (s ^ "\n" ^ List.fold_right debug_aux (t::env) "")
@@ -64,8 +64,8 @@ let whd context =
            C.Constant _ -> raise ReferenceToConstant
          | C.CurrentProof _ -> raise ReferenceToCurrentProof
          | C.InductiveDefinition _ -> raise ReferenceToInductiveDefinition
-         | C.Variable (_,None,_,_) -> if l = [] then t else C.Appl (t::l)
-         | C.Variable (_,Some body,_,_) ->
+         | C.Variable (_,None,_,_,_) -> if l = [] then t else C.Appl (t::l)
+         | C.Variable (_,Some body,_,_,_) ->
             whdaux l (CicSubstitution.subst_vars exp_named_subst body)
        )
     | C.Meta _ as t -> if l = [] then t else C.Appl (t::l)
@@ -87,11 +87,11 @@ let whd context =
          CicEnvironment.get_cooked_obj ~trust:false CicUniv.empty_ugraph uri
        in
        (match o with
-           C.Constant (_,Some body,_,_) ->
+           C.Constant (_,Some body,_,_,_) ->
             whdaux l (CicSubstitution.subst_vars exp_named_subst body)
          | C.Constant _ -> if l = [] then t else C.Appl (t::l)
          | C.Variable _ -> raise ReferenceToVariable
-         | C.CurrentProof (_,_,body,_,_) ->
+         | C.CurrentProof (_,_,body,_,_,_) ->
             whdaux l (CicSubstitution.subst_vars exp_named_subst body)
          | C.InductiveDefinition _ -> raise ReferenceToInductiveDefinition
        )
@@ -128,7 +128,7 @@ let whd context =
              let (arity, r) =
               let o,_ = CicEnvironment.get_obj CicUniv.empty_ugraph mutind in
               match o with
-                 C.InductiveDefinition (tl,ingredients,r) ->
+                 C.InductiveDefinition (tl,ingredients,r,_) ->
                    let (_,_,arity,_) = List.nth tl i in
                     (arity,r)
                | _ -> raise WrongUriToInductiveDefinition

diff --git a/helm/ocaml/cic_proof_checking/cicSubstitution.ml b/helm/ocaml/cic_proof_checking/cicSubstitution.ml
index a7124d4a3186d6512014c0f37a6e695e884401c1..431fa4b50d1303c6b64a3a90462fea9f3fd8d90f 100644 (file)
--- a/helm/ocaml/cic_proof_checking/cicSubstitution.ml
+++ b/helm/ocaml/cic_proof_checking/cicSubstitution.ml
@@ -208,7 +208,7 @@ prerr_endline ("@@@POSSIBLE BUG: SUBSTITUTION IS NOT SIMULTANEOUS") ;
            let obj,_ = CicEnvironment.get_obj CicUniv.empty_ugraph uri in
            (match obj with
                C.Constant _ -> raise ReferenceToConstant
-             | C.Variable (_,_,_,params) -> params
+             | C.Variable (_,_,_,params,_) -> params
              | C.CurrentProof _ -> raise ReferenceToCurrentProof
              | C.InductiveDefinition _ -> raise ReferenceToInductiveDefinition
            )
@@ -256,9 +256,9 @@ prerr_endline "---- END\n\n " ;
        let params =
         let obj,_ = CicEnvironment.get_obj CicUniv.empty_ugraph uri in
         (match obj with
-            C.Constant (_,_,_,params) -> params
+            C.Constant (_,_,_,params,_) -> params
           | C.Variable _ -> raise ReferenceToVariable
-          | C.CurrentProof (_,_,_,_,params) -> params
+          | C.CurrentProof (_,_,_,_,params,_) -> params
           | C.InductiveDefinition _ -> raise ReferenceToInductiveDefinition
         )
        in
@@ -273,7 +273,7 @@ prerr_endline "---- END\n\n " ;
             C.Constant _ -> raise ReferenceToConstant
           | C.Variable _ -> raise ReferenceToVariable
           | C.CurrentProof _ -> raise ReferenceToCurrentProof
-          | C.InductiveDefinition (_,params,_) -> params
+          | C.InductiveDefinition (_,params,_,_) -> params
         )
        in
         let exp_named_subst'' =
@@ -287,7 +287,7 @@ prerr_endline "---- END\n\n " ;
             C.Constant _ -> raise ReferenceToConstant
           | C.Variable _ -> raise ReferenceToVariable
           | C.CurrentProof _ -> raise ReferenceToCurrentProof
-          | C.InductiveDefinition (_,params,_) -> params
+          | C.InductiveDefinition (_,params,_,_) -> params
         )
        in
         let exp_named_subst'' =

diff --git a/helm/ocaml/cic_proof_checking/cicTypeChecker.ml b/helm/ocaml/cic_proof_checking/cicTypeChecker.ml
index cab4640c89ecb8d7e73cdd3c61d3fbe3af597375..2a7f8c4ae16ed82a9c7800df1345577cae5756fb 100644 (file)
--- a/helm/ocaml/cic_proof_checking/cicTypeChecker.ml
+++ b/helm/ocaml/cic_proof_checking/cicTypeChecker.ml
@@ -36,7 +36,7 @@ let debug t context =
  let rec debug_aux t i =
   let module C = Cic in
   let module U = UriManager in
-   CicPp.ppobj (C.Variable ("DEBUG", None, t, [])) ^ "\n" ^ i
+   CicPp.ppobj (C.Variable ("DEBUG", None, t, [], [])) ^ "\n" ^ i
  in
   if !fdebug = 0 then
    raise (TypeCheckerFailure (List.fold_right debug_aux (t::context) ""))
@@ -136,7 +136,7 @@ let rec type_of_constant ~logger uri ugraph =
 
        let ugraph_dust = 
          (match uobj with
-           C.Constant (_,Some te,ty,_) ->
+           C.Constant (_,Some te,ty,_,_) ->
            let _,ugraph = type_of ~logger ty ugraph in
            let type_of_te,ugraph' = type_of ~logger te ugraph in
               let b',ugraph'' = (R.are_convertible [] type_of_te ty ugraph') in
@@ -147,11 +147,11 @@ let rec type_of_constant ~logger uri ugraph =
                 (CicPp.ppterm ty)))
               else
                 ugraph'
-         | C.Constant (_,None,ty,_) ->
+         | C.Constant (_,None,ty,_,_) ->
            (* only to check that ty is well-typed *)
            let _,ugraph' = type_of ~logger ty ugraph in 
            ugraph'
-         | C.CurrentProof (_,conjs,te,ty,_) ->
+         | C.CurrentProof (_,conjs,te,ty,_,_) ->
              let _,ugraph1 =
               List.fold_left
                (fun (metasenv,ugraph) ((_,context,ty) as conj) ->
@@ -188,8 +188,8 @@ let rec type_of_constant ~logger uri ugraph =
           uobj,ugraph_dust       
   in
    match cobj,ugraph with
-      (C.Constant (_,_,ty,_)),g -> ty,g
-    | (C.CurrentProof (_,_,_,ty,_)),g -> ty,g
+      (C.Constant (_,_,ty,_,_)),g -> ty,g
+    | (C.CurrentProof (_,_,_,ty,_,_)),g -> ty,g
     | _ ->
         raise (TypeCheckerFailure ("Unknown constant:" ^ U.string_of_uri uri))
 
@@ -199,8 +199,8 @@ and type_of_variable ~logger uri ugraph =
  let module U = UriManager in
   (* 0 because a variable is never cooked => no partial cooking at one level *)
   match CicEnvironment.is_type_checked ~trust:true ugraph uri with
-     CicEnvironment.CheckedObj ((C.Variable (_,_,ty,_)),ugraph') -> ty,ugraph'
-   | CicEnvironment.UncheckedObj (C.Variable (_,bo,ty,_)) ->
+     CicEnvironment.CheckedObj ((C.Variable (_,_,ty,_,_)),ugraph') -> ty,ugraph'
+   | CicEnvironment.UncheckedObj (C.Variable (_,bo,ty,_,_)) ->
       logger#log (`Start_type_checking uri) ;
       (* only to check that ty is well-typed *)
       let _,ugraph1 = type_of ~logger ty ugraph in
@@ -220,7 +220,7 @@ and type_of_variable ~logger uri ugraph =
           CicEnvironment.set_type_checking_info uri ;
           logger#log (`Type_checking_completed uri) ;
           match CicEnvironment.is_type_checked ~trust:false ugraph uri with
-               CicEnvironment.CheckedObj ((C.Variable (_,_,ty,_)),ugraph') -> 
+               CicEnvironment.CheckedObj ((C.Variable (_,_,ty,_,_)),ugraph') -> 
                 ty,ugraph'
             | CicEnvironment.CheckedObj _ 
              | CicEnvironment.UncheckedObj _ -> raise CicEnvironmentError
@@ -406,7 +406,7 @@ and strictly_positive context n nn te =
       let (ok,paramsno,ity,cl,name) =
        let o,_ = CicEnvironment.get_obj CicUniv.empty_ugraph uri in
        match o with
-           C.InductiveDefinition (tl,_,paramsno) ->
+           C.InductiveDefinition (tl,_,paramsno,_) ->
             let (name,_,ity,cl) = List.nth tl i in
              (List.length tl = 1, paramsno, ity, cl, name)
          | _ ->
@@ -545,7 +545,7 @@ and typecheck_mutual_inductive_defs ~logger uri (itl,_,indparamsno) ugraph =
 (* inductive block definition.                         *)
 and check_mutual_inductive_defs uri obj ugraph =
   match obj with
-      Cic.InductiveDefinition (itl, params, indparamsno) ->
+      Cic.InductiveDefinition (itl, params, indparamsno, _) ->
        typecheck_mutual_inductive_defs uri (itl,params,indparamsno) ugraph 
     | _ ->
        raise (TypeCheckerFailure (
@@ -578,7 +578,7 @@ and type_of_mutual_inductive_defs ~logger uri i ugraph =
                 uobj,ugraph1_dust
   in
     match cobj with
-       C.InductiveDefinition (dl,_,_) ->
+       C.InductiveDefinition (dl,_,_,_) ->
          let (_,_,arity,_) = List.nth dl i in
            arity,ugraph1
       | _ ->
@@ -613,7 +613,7 @@ and type_of_mutual_inductive_constr ~logger uri i j ugraph =
                  uobj,ugraph1_dust
   in
     match cobj with
-       C.InductiveDefinition (dl,_,_) ->
+       C.InductiveDefinition (dl,_,_,_) ->
          let (_,_,_,cl) = List.nth dl i in
           let (_,ty) = List.nth cl (j-1) in
             ty,ugraph1
@@ -742,7 +742,7 @@ and check_is_really_smaller_arg ?(subst = []) context n nn kl x safes te =
            let (tys,len,isinductive,paramsno,cl) =
            let o,_ = CicEnvironment.get_obj CicUniv.empty_ugraph uri in
             match o with
-               C.InductiveDefinition (tl,_,paramsno) ->
+               C.InductiveDefinition (tl,_,paramsno,_) ->
                 let tys =
                  List.map
                   (fun (n,_,ty,_) -> Some (Cic.Name n,(Cic.Decl ty))) tl
@@ -781,7 +781,7 @@ and check_is_really_smaller_arg ?(subst = []) context n nn kl x safes te =
            let (tys,len,isinductive,paramsno,cl) =
             let o,_ = CicEnvironment.get_obj CicUniv.empty_ugraph uri in
             match o with
-               C.InductiveDefinition (tl,_,paramsno) ->
+               C.InductiveDefinition (tl,_,paramsno,_) ->
                 let (_,isinductive,_,cl) = List.nth tl i in
                  let tys =
                   List.map (fun (n,_,ty,_) ->
@@ -908,7 +908,7 @@ and guarded_by_destructors ?(subst = []) context n nn kl x safes =
            let (tys,len,isinductive,paramsno,cl) =
            let o,_ = CicEnvironment.get_obj CicUniv.empty_ugraph uri in
             match o with
-               C.InductiveDefinition (tl,_,paramsno) ->
+               C.InductiveDefinition (tl,_,paramsno,_) ->
                 let len = List.length tl in
                  let (_,isinductive,_,cl) = List.nth tl i in
                   let tys =
@@ -953,7 +953,7 @@ and guarded_by_destructors ?(subst = []) context n nn kl x safes =
            let (tys,len,isinductive,paramsno,cl) =
            let o,_ = CicEnvironment.get_obj CicUniv.empty_ugraph uri in
             match o with
-               C.InductiveDefinition (tl,_,paramsno) ->
+               C.InductiveDefinition (tl,_,paramsno,_) ->
                 let (_,isinductive,_,cl) = List.nth tl i in
                  let tys =
                   List.map
@@ -1068,7 +1068,7 @@ and guarded_by_constructors context n nn h te args coInductiveTypeURI =
          with Not_found -> assert false
        in
        match obj with
-          C.InductiveDefinition (itl,_,_) ->
+          C.InductiveDefinition (itl,_,_,_) ->
            let (_,_,_,cl) = List.nth itl i in
             let (_,cons) = List.nth cl (j - 1) in
              CicSubstitution.subst_vars exp_named_subst cons
@@ -1253,7 +1253,7 @@ and check_allowed_sort_elimination ~logger context uri i need_dummy ind
 (*CSC: WRONG. MISSING CONDITIONS ON THE ARGUMENTS OF THE CONSTRUTOR *)
        (let o,_ = CicEnvironment.get_obj CicUniv.empty_ugraph uri in
         match o with
-         C.InductiveDefinition (itl,_,_) ->
+         C.InductiveDefinition (itl,_,_,_) ->
            let (_,_,_,cl) = List.nth itl i in
            (* is a singleton definition or the empty proposition? *)
            (List.length cl = 1 || List.length cl = 0) , ugraph
@@ -1273,7 +1273,7 @@ and check_allowed_sort_elimination ~logger context uri i need_dummy ind
       when need_dummy ->
        (let o,_ = CicEnvironment.get_obj CicUniv.empty_ugraph uri in
         match o with
-           C.InductiveDefinition (itl,_,paramsno) ->
+           C.InductiveDefinition (itl,_,paramsno,_) ->
             let tys =
              List.map (fun (n,_,ty,_) -> Some (Cic.Name n,(Cic.Decl ty))) itl
             in
@@ -1301,7 +1301,7 @@ and check_allowed_sort_elimination ~logger context uri i need_dummy ind
          | (C.Sort C.Set | C.Sort C.CProp) ->
              (let o,_ = CicEnvironment.get_obj CicUniv.empty_ugraph uri in
               match o with
-               C.InductiveDefinition (itl,_,_) ->
+               C.InductiveDefinition (itl,_,_,_) ->
                    let (_,_,_,cl) = List.nth itl i in
                    (* is a singleton definition? *)
                    List.length cl = 1,ugraph1
@@ -1327,7 +1327,7 @@ and check_allowed_sort_elimination ~logger context uri i need_dummy ind
              (* TASSI: da verificare *)
              (let o,_ = CicEnvironment.get_obj CicUniv.empty_ugraph uri in
               match o with
-               C.InductiveDefinition (itl,_,paramsno) ->
+               C.InductiveDefinition (itl,_,paramsno,_) ->
                  let (_,_,_,cl) = List.nth itl i in
                  let tys =
                    List.map
@@ -1727,7 +1727,7 @@ and type_of_aux' ~logger ?(subst = []) metasenv context t ugraph =
           with Not_found -> assert false
         in
         match obj with
-            C.InductiveDefinition (_,_,parsno) -> parsno
+            C.InductiveDefinition (_,_,parsno,_) -> parsno
           | _ ->
               raise (TypeCheckerFailure
                 ("Unknown mutual inductive definition:" ^
@@ -1966,7 +1966,7 @@ and type_of_aux' ~logger ?(subst = []) metasenv context t ugraph =
           with Not_found -> assert false
         in
         (match obj with
-           C.InductiveDefinition (itl,_,_) ->
+           C.InductiveDefinition (itl,_,_,_) ->
             let (_,is_inductive,_,_) = List.nth itl i in
              if is_inductive then None else (Some uri)
          | _ ->
@@ -1977,7 +1977,7 @@ and type_of_aux' ~logger ?(subst = []) metasenv context t ugraph =
     | C.Appl ((C.MutInd (uri,i,_))::_) ->
        (let o,_ = CicEnvironment.get_obj CicUniv.empty_ugraph uri in
         match o with
-           C.InductiveDefinition (itl,_,_) ->
+           C.InductiveDefinition (itl,_,_,_) ->
             let (_,is_inductive,_,_) = List.nth itl i in
              if is_inductive then None else (Some uri)
          | _ ->
@@ -2045,7 +2045,7 @@ let typecheck uri ugraph =
       (* prerr_endline ("INIZIO A TYPECHECKARE " ^ U.string_of_uri uri); *)
       let ugraph1 = 
        (match uobj with
-         C.Constant (_,Some te,ty,_) ->
+         C.Constant (_,Some te,ty,_,_) ->
            let _,ugraph1 = type_of ~logger ty ugraph in
           let ty_te,ugraph2 = type_of ~logger te ugraph1 in
            let b,ugraph3 = (R.are_convertible [] ty_te ty ugraph2) in
@@ -2054,11 +2054,11 @@ let typecheck uri ugraph =
                 ("Unknown constant:" ^ U.string_of_uri uri))
            else
              ugraph3
-        | C.Constant (_,None,ty,_) ->
+        | C.Constant (_,None,ty,_,_) ->
           (* only to check that ty is well-typed *)
           let _,ugraph1 = type_of ~logger ty ugraph in
          ugraph1
-        | C.CurrentProof (_,conjs,te,ty,_) ->
+        | C.CurrentProof (_,conjs,te,ty,_,_) ->
            let _,ugraph1 =
             List.fold_left
              (fun (metasenv,ugraph) ((_,context,ty) as conj) ->
@@ -2080,7 +2080,7 @@ let typecheck uri ugraph =
                 (CicPp.ppterm ty)))
            else
              ugraph4
-        | C.Variable (_,bo,ty,_) ->
+        | C.Variable (_,bo,ty,_,_) ->
            (* only to check that ty is well-typed *)
            let _,ugraph1 = type_of ~logger ty ugraph in
             (match bo with

diff --git a/helm/ocaml/cic_proof_checking/cicUnivUtils.ml b/helm/ocaml/cic_proof_checking/cicUnivUtils.ml
index c027194543abc4cc0d4bc5aa4aa448eb7d996bf4..a7861444ef5c43d4961d5a7f790fea67b8acfa08 100644 (file)
--- a/helm/ocaml/cic_proof_checking/cicUnivUtils.ml
+++ b/helm/ocaml/cic_proof_checking/cicUnivUtils.ml
@@ -54,7 +54,7 @@ let universes_of_obj uri t =
            don := u::!don;
             (match fst(CicEnvironment.get_obj CicUniv.empty_ugraph u)
               with
-               | C.InductiveDefinition (l,_,_) -> 
+               | C.InductiveDefinition (l,_,_,_) -> 
                   List.fold_left (
                     fun y (_,_,t,l') -> 
                       y @ (aux t) @ 
@@ -72,7 +72,7 @@ let universes_of_obj uri t =
          begin
            don := u::!don;
            (match fst(CicEnvironment.get_obj CicUniv.empty_ugraph u) with
-              | C.InductiveDefinition (l,_,_) -> 
+              | C.InductiveDefinition (l,_,_,_) -> 
                   List.fold_left (
                     fun x (_,_,_t,l') ->
                       x @ aux t @  
@@ -113,37 +113,37 @@ let universes_of_obj uri t =
        List.fold_left (fun x (_,b,c) -> x @ (aux b) @ (aux c)) [] funs
   and aux_obj ?(boo=false) (t,_)  = 
     (match t with
-        C.Constant (_,Some te,ty,v) -> aux te @ aux ty @
+        C.Constant (_,Some te,ty,v,_) -> aux te @ aux ty @
            List.fold_left (
              fun l u ->
                l @ if eq u uri then [] else 
                  (aux_obj (CicEnvironment.get_obj CicUniv.empty_ugraph u)))
           [] v
-       | C.Constant (_,None,ty,v) -> aux ty @
+       | C.Constant (_,None,ty,v,_) -> aux ty @
            List.fold_left (
              fun l u ->
                l @ if eq u uri then [] else 
                  (aux_obj (CicEnvironment.get_obj CicUniv.empty_ugraph u)))
             [] v
-       | C.CurrentProof (_,conjs,te,ty,v) -> aux te @ aux ty @
+       | C.CurrentProof (_,conjs,te,ty,v,_) -> aux te @ aux ty @
            List.fold_left (
              fun l u ->
                l @ if eq u uri then [] else 
                  (aux_obj (CicEnvironment.get_obj CicUniv.empty_ugraph u)))
             [] v
-       | C.Variable (_,Some bo,ty,v) -> aux bo @ aux ty @
+       | C.Variable (_,Some bo,ty,v,_) -> aux bo @ aux ty @
            List.fold_left (
              fun l u ->
                l @ if eq u uri then [] else 
                  (aux_obj (CicEnvironment.get_obj CicUniv.empty_ugraph u)))
             [] v
-       | C.Variable (_,None ,ty,v) -> aux ty @ 
+       | C.Variable (_,None ,ty,v,_) -> aux ty @ 
            List.fold_left (
              fun l u ->
                l @ if eq u uri then [] else 
                  (aux_obj (CicEnvironment.get_obj CicUniv.empty_ugraph u)))
             [] v
-       | C.InductiveDefinition (l,v,_) -> 
+       | C.InductiveDefinition (l,v,_,_) -> 
           (List.fold_left (
              fun x (_,_,t,l') ->
                x @ aux t @ List.fold_left (

diff --git a/helm/ocaml/cic_unification/cicRefine.ml b/helm/ocaml/cic_unification/cicRefine.ml
index 24171327c80adce776de9ada770c26ffd62e43fc..fe70f250aa89999161824cf26d08639dc18739a7 100644 (file)
--- a/helm/ocaml/cic_unification/cicRefine.ml
+++ b/helm/ocaml/cic_unification/cicRefine.ml
@@ -76,8 +76,8 @@ let rec type_of_constant uri ugraph =
     *)
   let obj,u= CicEnvironment.get_obj ugraph uri in
     match obj with
-       C.Constant (_,_,ty,_) -> ty,u
-      | C.CurrentProof (_,_,_,ty,_) -> ty,u
+       C.Constant (_,_,ty,_,_) -> ty,u
+      | C.CurrentProof (_,_,_,ty,_,_) -> ty,u
       | _ ->
          raise
            (RefineFailure ("Unknown constant definition " ^  U.string_of_uri uri))
@@ -95,7 +95,7 @@ and type_of_variable uri ugraph =
     *)
   let obj,u = CicEnvironment.get_obj ugraph uri in
     match obj with
-       C.Variable (_,_,ty,_) -> ty,u
+       C.Variable (_,_,ty,_,_) -> ty,u
       |  _ ->
           raise
            (RefineFailure
@@ -114,7 +114,7 @@ and type_of_mutual_inductive_defs uri i ugraph =
     *)
   let obj,u = CicEnvironment.get_obj ugraph uri in
     match obj with
-       C.InductiveDefinition (dl,_,_) ->
+       C.InductiveDefinition (dl,_,_,_) ->
          let (_,_,arity,_) = List.nth dl i in
            arity,u
       | _ ->
@@ -135,7 +135,7 @@ and type_of_mutual_inductive_constr uri i j ugraph =
     *)
   let obj,u = CicEnvironment.get_obj ugraph uri in
     match obj with
-       C.InductiveDefinition (dl,_,_) ->
+       C.InductiveDefinition (dl,_,_,_) ->
          let (_,_,_,cl) = List.nth dl i in
           let (_,ty) = List.nth cl (j-1) in
             ty,u
@@ -366,7 +366,7 @@ and type_of_aux' metasenv context t ugraph =
              *)
              let obj,u = CicEnvironment.get_obj ugraph uri in
               match obj with
-                 C.InductiveDefinition (l,expl_params,parsno) -> 
+                 C.InductiveDefinition (l,expl_params,parsno,_) -> 
                    List.nth l i , expl_params, parsno, u
                | _ ->
                    raise

diff --git a/helm/ocaml/cic_unification/coercGraph.ml b/helm/ocaml/cic_unification/coercGraph.ml
index 4dd05073b26b3ab2af09899254f7713a6a25a22c..e01f28eb3fcc1994f068dbc86926e6dff42a614c 100644 (file)
--- a/helm/ocaml/cic_unification/coercGraph.ml
+++ b/helm/ocaml/cic_unification/coercGraph.ml
@@ -94,7 +94,7 @@ let get_closure_coercions src tgt uri =
     [] c_to_src)
 ;;
 
-      
+let obj_attrs = [`Class `Coercion; `Generated]
 
 (* generate_composite_closure (c2 (c1 s)) in the universe graph univ *)
 let generate_composite_closure c1 c2 univ =
@@ -129,7 +129,7 @@ let generate_composite_closure c1 c2 univ =
   let cleaned_ty =
     FreshNamesGenerator.clean_dummy_dependent_types c_ty 
   in
-  let obj = Cic.Constant ("xxxx",Some c,cleaned_ty,[]) in 
+  let obj = Cic.Constant ("xxxx",Some c,cleaned_ty,[],obj_attrs) in 
     obj,univ
 ;;
 
@@ -161,13 +161,14 @@ let close_coercion_graph src tgt uri =
                 CicUtil.term_of_uri (UriManager.string_of_uri uri)
               in
               let first_step = 
-                (Cic.Constant ("",Some (term_of_uri' he),Cic.Sort Cic.Prop,[]))
+                Cic.Constant ("", Some (term_of_uri' he), Cic.Sort Cic.Prop, [],
+                  obj_attrs)
               in
               let o,u = 
                 List.fold_left (fun (o,u) coer ->
                   match o with 
-                  |  Cic.Constant (_,Some c,_,[]) ->
-                    generate_composite_closure c (term_of_uri' coer) u
+                  | Cic.Constant (_,Some c,_,[],_) ->
+                      generate_composite_closure c (term_of_uri' coer) u
                   | _ -> assert false 
                 ) (first_step, CicUniv.empty_ugraph) tl
               in
@@ -180,7 +181,8 @@ let close_coercion_graph src tgt uri =
               in
               let named_obj = 
                 match o with
-                | Cic.Constant (_,bo,ty,vl) -> Cic.Constant (name,bo,ty,vl)
+                | Cic.Constant (_,bo,ty,vl,attrs) ->
+                    Cic.Constant (name,bo,ty,vl,attrs)
                 | _ -> assert false 
               in
                 ((src,tgt,c_uri),(c_uri,named_obj,u))