]> matita.cs.unibo.it Git - helm.git/blobdiff - helm/software/components/acic_content/content.ml
metavariable context has a separator now
[helm.git] / helm / software / components / acic_content / content.ml
index c8b22f497e713cd0186d99e720ebdd93739fad5c..1e4cc88afa1532040ec534ae4c0560fe28999502 100644 (file)
@@ -58,7 +58,8 @@ type 'term definition =
        { def_name : string option;
          def_id : id ;
          def_aref : string ;
-         def_term : 'term 
+         def_term : 'term ;
+         def_type : 'term 
        }
 ;;