X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fmatita%2Fhelp%2FC%2Fsec_intro.xml;h=6c22f46647fe4dad91567fefc8f3af95c5b82634;hb=65317d14f32bc24b3e9ed4ea144833dd8517773a;hp=773bda24ca7f86fe0e0cba580a3e5f6e103d6b98;hpb=871ed1c297e8c929a8c4460162e8521c9656bbc0;p=helm.git diff --git a/helm/software/matita/help/C/sec_intro.xml b/helm/software/matita/help/C/sec_intro.xml index 773bda24c..6c22f4664 100644 --- a/helm/software/matita/help/C/sec_intro.xml +++ b/helm/software/matita/help/C/sec_intro.xml @@ -9,7 +9,7 @@ (or proof assistant) with the following characteristics: - It is based on a variant of the Calculus of (co)Inductive Constructions (CIC). CIC is also the logic of the Coq proof assistant. + It is based on a variant of the Calculus of (Co)Inductive Constructions (CIC). CIC is also the logic of the Coq proof assistant. It adopts a procedural proof language, but it has a new set of small step tacticals that improve proof structuring and debugging.